---

Step * 2 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}
⊢ g is Q1-R-pre-preserving on {Ib}
BY
{ ((RWO "12" 0 THEN Auto) THEN (All (es_pred_rewrite) THEN Auto) THEN Auto)⋅ }

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. Q1 ⇐⇒ Q2
⊢ ...GenFormulaCondC: failed... Q1 ⇐⇒ Q2

---

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\}
\mvdash{}  g  is  Q1-R-pre-preserving  on  \{Ib\}


By

---

Latex:
((RWO  "12"  0  THEN  Auto)  THEN  (All  (es\_pred\_rewrite)  THEN  Auto)  THEN  Auto)\mcdot{}

---

Home Index