---

Step * 2 1 2 1 of Lemma Q-R-glues_functionality


1. Info : Type
2. es : EO+(Info)@i'
3. R : E ⟶ E ⟶ ℙ
4. A : Type
5. B : Type
6. Ia : EClass(A)@i'
7. Ib : EClass(B)@i'
8. f : E(Ia) ⟶ B@i
9. Q1 : E ⟶ E ⟶ ℙ
10. Q2 : E ⟶ E ⟶ ℙ
11. g : E(Ib) ⟶ E@i
12. Q1 ⇐⇒ Q2@i
13. {Ia} ←←= g== {Ib}@i
14. g is Q2-R-pre-preserving on {Ib}@i
15. Inj(E(Ib);E;g)@i
16. ∀e:E(Ib). ((f (g e)) = Ib(e) ∈ B)@i
17. {Ia} ←←= g== {Ib}
18. ∀x,y:E(Ia).  (Q1 x y ⇐⇒ Q2 x y)
19. x : {e:E| ∃x:E(Ib). (e = (g x) ∈ E)} @i
20. ∀y:E(Ia). (Q1 x y ⇐⇒ Q2 x y)
21. y : E@i
22. x1 : E(Ib)@i
23. y = (g x1) ∈ E@i
24. g ∈ E(Ib) ⟶ E(Ia)
⊢ y ∈ E(Ia)
BY
{ (All (Unfold `es-E-interface`)
   THEN (MemTypeCD THEN Auto)
   THEN HypSubst' -2 0
   THEN Auto
   THEN GenConclAtAddr [1;3]
   THEN D -2
   THEN Unhide
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  R  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  A  :  Type
5.  B  :  Type
6.  Ia  :  EClass(A)@i'
7.  Ib  :  EClass(B)@i'
8.  f  :  E(Ia)  {}\mrightarrow{}  B@i
9.  Q1  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
10.  Q2  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
11.  g  :  E(Ib)  {}\mrightarrow{}  E@i
12.  Q1  \mLeftarrow{}{}\mRightarrow{}  Q2@i
13.  \{Ia\}  \mleftarrow{}\mleftarrow{}=  g==  \{Ib\}@i
14.  g  is  Q2-R-pre-preserving  on  \{Ib\}@i
15.  Inj(E(Ib);E;g)@i
16.  \mforall{}e:E(Ib).  ((f  (g  e))  =  Ib(e))@i
17.  \{Ia\}  \mleftarrow{}\mleftarrow{}=  g==  \{Ib\}
18.  \mforall{}x,y:E(Ia).    (Q1  x  y  \mLeftarrow{}{}\mRightarrow{}  Q2  x  y)
19.  x  :  \{e:E|  \mexists{}x:E(Ib).  (e  =  (g  x))\}  @i
20.  \mforall{}y:E(Ia).  (Q1  x  y  \mLeftarrow{}{}\mRightarrow{}  Q2  x  y)
21.  y  :  E@i
22.  x1  :  E(Ib)@i
23.  y  =  (g  x1)@i
24.  g  \mmember{}  E(Ib)  {}\mrightarrow{}  E(Ia)
\mvdash{}  y  \mmember{}  E(Ia)


By

---

Latex:
(All  (Unfold  `es-E-interface`)
  THEN  (MemTypeCD  THEN  Auto)
  THEN  HypSubst'  -2  0
  THEN  Auto
  THEN  GenConclAtAddr  [1;3]
  THEN  D  -2
  THEN  Unhide
  THEN  Auto)\mcdot{}

---

Home Index