Step * 2 of Lemma Q-R-glues-composes


1. [Info] Type
2. es EO+(Info)@i'
3. [Qa] E ─→ E ─→ ℙ
4. [Rb] E ─→ E ─→ ℙ
5. [Sc] E ─→ E ─→ ℙ
6. [A] Type
7. [B] Type
8. [C] Type
9. Ia EClass(A)@i'
10. Ib EClass(B)@i'
11. Ic EClass(C)@i'
12. f1 E(Ia) ─→ B@i
13. f2 B ─→ C@i
14. g1 E(Ib) ─→ E(Ia)@i
15. g2 E(Ic) ─→ E(Ib)@i
16. λe.(↑e ∈b Ia) ←←g1== λe.(↑e ∈b Ib)@i
17. g1 is Qa-Rb-pre-preserving on λe.(↑e ∈b Ib)@i
18. Inj(E(Ib);E;g1)@i
19. ∀e:E(Ib). ((f1 (g1 e)) Ib(e) ∈ B)@i
20. λe.(↑e ∈b Ib) ←←g2== λe.(↑e ∈b Ic)@i
21. g2 is Rb-Sc-pre-preserving on λe.(↑e ∈b Ic)@i
22. Inj(E(Ic);E;g2)@i
23. ∀e:E(Ic). ((f2 Ib(g2 e)) Ic(e) ∈ C)@i
24. λe.(↑e ∈b Ia) ←←g1 g2== λe.(↑e ∈b Ic)
⊢ g1 g2 is Qa-Sc-pre-preserving on λe.(↑e ∈b Ic)
BY
(Using [`Q2',⌈Rb⌉`P2',⌈λe.(↑e ∈b Ib)⌉]  (BLemma `Q-R-pre-preserving-compose`)⋅
   THEN Auto
   THEN Reduce 0
   THEN Try (Complete (Auto))) }


Latex:



Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  [Qa]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  [Rb]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  [Sc]  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
6.  [A]  :  Type
7.  [B]  :  Type
8.  [C]  :  Type
9.  Ia  :  EClass(A)@i'
10.  Ib  :  EClass(B)@i'
11.  Ic  :  EClass(C)@i'
12.  f1  :  E(Ia)  {}\mrightarrow{}  B@i
13.  f2  :  B  {}\mrightarrow{}  C@i
14.  g1  :  E(Ib)  {}\mrightarrow{}  E(Ia)@i
15.  g2  :  E(Ic)  {}\mrightarrow{}  E(Ib)@i
16.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)  \mleftarrow{}\mleftarrow{}=  g1==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)@i
17.  g1  is  Qa-Rb-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)@i
18.  Inj(E(Ib);E;g1)@i
19.  \mforall{}e:E(Ib).  ((f1  (g1  e))  =  Ib(e))@i
20.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)  \mleftarrow{}\mleftarrow{}=  g2==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)@i
21.  g2  is  Rb-Sc-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)@i
22.  Inj(E(Ic);E;g2)@i
23.  \mforall{}e:E(Ic).  ((f2  Ib(g2  e))  =  Ic(e))@i
24.  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ia)  \mleftarrow{}\mleftarrow{}=  g1  o  g2==  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)
\mvdash{}  g1  o  g2  is  Qa-Sc-pre-preserving  on  \mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ic)


By


Latex:
(Using  [`Q2',\mkleeneopen{}Rb\mkleeneclose{};  `P2',\mkleeneopen{}\mlambda{}e.(\muparrow{}e  \mmember{}\msubb{}  Ib)\mkleeneclose{}]    (BLemma  `Q-R-pre-preserving-compose`)\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto)))




Home Index