---

Step * 1 2 1 1 1 1 1 of Lemma weak-antecedent-surjections-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. Q ←==f== P@i
8. ∀e:{e:E| Q e} . ∃e':{e:E| P e} . ((f e') = e ∈ E)@i
9. R ←==g== Q@i
10. ∀e:{e:E| R e} . ∃e':{e:E| Q e} . ((g e') = e ∈ E)@i
11. e : {e:E| R e} @i
12. e' : {e:E| Q e} 
13. (g e') = e ∈ E
14. e'@0 : {e:E| P e} 
15. (f e'@0) = e' ∈ E
⊢ ((g o f) e'@0) = e ∈ E
BY
{ RepUR ``compose`` 0 }

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. Q ←==f== P@i
8. ∀e:{e:E| Q e} . ∃e':{e:E| P e} . ((f e') = e ∈ E)@i
9. R ←==g== Q@i
10. ∀e:{e:E| R e} . ∃e':{e:E| Q e} . ((g e') = e ∈ E)@i
11. e : {e:E| R e} @i
12. e' : {e:E| Q e} 
13. (g e') = e ∈ E
14. e'@0 : {e:E| P e} 
15. (f e'@0) = e' ∈ E
⊢ (g (f e'@0)) = e ∈ 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.  Q  \mleftarrow{}==f==  P@i
8.  \mforall{}e:\{e:E|  Q  e\}  .  \mexists{}e':\{e:E|  P  e\}  .  ((f  e')  =  e)@i
9.  R  \mleftarrow{}==g==  Q@i
10.  \mforall{}e:\{e:E|  R  e\}  .  \mexists{}e':\{e:E|  Q  e\}  .  ((g  e')  =  e)@i
11.  e  :  \{e:E|  R  e\}  @i
12.  e'  :  \{e:E|  Q  e\} 
13.  (g  e')  =  e
14.  e'@0  :  \{e:E|  P  e\} 
15.  (f  e'@0)  =  e'
\mvdash{}  ((g  o  f)  e'@0)  =  e


By

RepUR  ``compose``  0

---

Home Index