---

Step * 1 of Lemma weak-antecedent-functions-compose


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))
BY
{ (InstHyp [⌈e⌉] (-3)⋅ 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
10. f e c≤ e ∧ (Q (f e))
⊢ (g o f) e c≤ e ∧ (R ((g o f) e))

---

Latex:



1.  es  :  EO@i'
2.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  [R]  :  E  {}\mrightarrow{}  \mBbbP{}
5.  f  :  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  @i
6.  g  :  \{e:E|  Q  e\}    {}\mrightarrow{}  \{e:E|  R  e\}  @i
7.  \mforall{}e:\{e:E|  P  e\}  .  (f  e  c\mleq{}  e  \mwedge{}  (Q  (f  e)))@i
8.  \mforall{}e:\{e:E|  Q  e\}  .  (g  e  c\mleq{}  e  \mwedge{}  (R  (g  e)))@i
9.  e  :  \{e:E|  P  e\}  @i
\mvdash{}  (g  o  f)  e  c\mleq{}  e  \mwedge{}  (R  ((g  o  f)  e))


By

(InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)

---

Home Index