---

Step * 1 of Lemma Q-R-pre-preserving-1-1


1. es : EO
2. P : E ⟶ ℙ
3. Q : E ⟶ E ⟶ ℙ
4. R : E ⟶ E ⟶ ℙ
5. f : {e:E| P e}  ⟶ E
6. ∀a:E. (Q a a)
7. ∀e,e':E.  ((R e e') ⇒ (R e' e) ⇒ (e = e' ∈ E))
8. ∀e,e':{e:E| P e} .  ((Q (f e) (f e')) ⇒ (R e e'))
9. a1 : {e:E| P e} @i
10. a2 : {e:E| P e} @i
11. (f a1) = (f a2) ∈ E@i
⊢ a1 = a2 ∈ {e:E| P e} 
BY
{ Assert ⌜(Q (f a1) (f a2)) ∧ (Q (f a2) (f a1))⌝⋅⋅ }

1
.....assertion..... 
1. es : EO
2. P : E ⟶ ℙ
3. Q : E ⟶ E ⟶ ℙ
4. R : E ⟶ E ⟶ ℙ
5. f : {e:E| P e}  ⟶ E
6. ∀a:E. (Q a a)
7. ∀e,e':E.  ((R e e') ⇒ (R e' e) ⇒ (e = e' ∈ E))
8. ∀e,e':{e:E| P e} .  ((Q (f e) (f e')) ⇒ (R e e'))
9. a1 : {e:E| P e} @i
10. a2 : {e:E| P e} @i
11. (f a1) = (f a2) ∈ E@i
⊢ (Q (f a1) (f a2)) ∧ (Q (f a2) (f a1))

2
1. es : EO
2. P : E ⟶ ℙ
3. Q : E ⟶ E ⟶ ℙ
4. R : E ⟶ E ⟶ ℙ
5. f : {e:E| P e}  ⟶ E
6. ∀a:E. (Q a a)
7. ∀e,e':E.  ((R e e') ⇒ (R e' e) ⇒ (e = e' ∈ E))
8. ∀e,e':{e:E| P e} .  ((Q (f e) (f e')) ⇒ (R e e'))
9. a1 : {e:E| P e} @i
10. a2 : {e:E| P e} @i
11. (f a1) = (f a2) ∈ E@i
12. (Q (f a1) (f a2)) ∧ (Q (f a2) (f a1))
⊢ a1 = a2 ∈ {e:E| P e} 

---

Latex:

---

Latex:

1.  es  :  EO
2.  P  :  E  {}\mrightarrow{}  \mBbbP{}
3.  Q  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
4.  R  :  E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
5.  f  :  \{e:E|  P  e\}    {}\mrightarrow{}  E
6.  \mforall{}a:E.  (Q  a  a)
7.  \mforall{}e,e':E.    ((R  e  e')  {}\mRightarrow{}  (R  e'  e)  {}\mRightarrow{}  (e  =  e'))
8.  \mforall{}e,e':\{e:E|  P  e\}  .    ((Q  (f  e)  (f  e'))  {}\mRightarrow{}  (R  e  e'))
9.  a1  :  \{e:E|  P  e\}  @i
10.  a2  :  \{e:E|  P  e\}  @i
11.  (f  a1)  =  (f  a2)@i
\mvdash{}  a1  =  a2


By

---

Latex:
Assert  \mkleeneopen{}(Q  (f  a1)  (f  a2))  \mwedge{}  (Q  (f  a2)  (f  a1))\mkleeneclose{}\mcdot{}\mcdot{}

---

Home Index