---

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

.....wf..... 
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:E| ∃x:E(Ib). (e = (g x) ∈ E)} @i
⊢ y ∈ E(Ia)
BY
{ (((FLemma `weak-antecedent-surjection-property` [13]) THENA (Auto THEN All es_pred_rewrite THEN Auto THEN Auto))
   THEN All es_pred_rewrite
   THEN DVar `y'
   THEN ExRepD) }

1
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)

---

Latex:

---

Latex:
.....wf..... 
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:E|  \mexists{}x:E(Ib).  (e  =  (g  x))\}  @i
\mvdash{}  y  \mmember{}  E(Ia)


By

---

Latex:
(((FLemma  `weak-antecedent-surjection-property`  [13])
    THENA  (Auto  THEN  All  es\_pred\_rewrite  THEN  Auto  THEN  Auto)
    )
  THEN  All  es\_pred\_rewrite
  THEN  DVar  `y'
  THEN  ExRepD)

---

Home Index