---

Step * 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. Q1 ⇐⇒ Q2
⊢ ...GenFormulaCondC: failed... Q1 ⇐⇒ Q2
BY
{ (Unfold `label` 0 THEN Repeat (ParallelLast) THEN Auto) }

1
.....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
⊢ x ∈ E(Ia)

2
.....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)

---

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.  Q1  \mLeftarrow{}{}\mRightarrow{}  Q2
\mvdash{}  ...GenFormulaCondC:  failed...  Q1  \mLeftarrow{}{}\mRightarrow{}  Q2


By

---

Latex:
(Unfold  `label`  0  THEN  Repeat  (ParallelLast)  THEN  Auto)

---

Home Index