---

Step * of Lemma weak-antecedent-functions-compose

∀es:EO
  ∀[P,Q,R:E ─→ ℙ].
    ∀f:{e:E| P e}  ─→ {e:E| Q e} . ∀g:{e:E| Q e}  ─→ {e:E| R e} .  ((Q ←==f== P ∧ R ←==g== Q) ⇒ R ←==g o f== P)
BY
{ ((Auto THEN All (Unfold `weak-antecedent-function`)) THEN (D 0 THENA Auto)) }

1
1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. [R] : E ─→ ℙ
5. f : {e:E| P e}  ─→ {e:E| Q e} @i
6. g : {e:E| Q e}  ─→ {e:E| R e} @i
7. ∀e:{e:E| P e} . (f e c≤ e ∧ (Q (f e)))@i
8. ∀e:{e:E| Q e} . (g e c≤ e ∧ (R (g e)))@i
9. e : {e:E| P e} @i
⊢ (g o f) e c≤ e ∧ (R ((g o f) e))

---

Latex:


\mforall{}es:EO
    \mforall{}[P,Q,R:E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  .  \mforall{}g:\{e:E|  Q  e\}    {}\mrightarrow{}  \{e:E|  R  e\}  .
            ((Q  \mleftarrow{}==f==  P  \mwedge{}  R  \mleftarrow{}==g==  Q)  {}\mRightarrow{}  R  \mleftarrow{}==g  o  f==  P)


By

((Auto  THEN  All  (Unfold  `weak-antecedent-function`))  THEN  (D  0  THENA  Auto))

---

Home Index