---

Step * 1 1 1 1 of Lemma implies-quotient-true2


1. Q : ℙ
2. v : Base
3. v2 : Base
4. v = v2 ∈ pertype(λx,y. ((x ∈ Q) ∧ (y ∈ Q) ∧ True))
5. v ∈ Q
6. v2 ∈ Q
7. True
8. v1 : Base
9. v3 : Base
10. v1 = v3 ∈ pertype(λx,y. ((x ∈ Q) ∧ (y ∈ Q) ∧ True))
11. v1 ∈ Q
12. v3 ∈ Q
13. True
⊢ v = v3 ∈ ⇃(Q)
BY
{ (EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  Q  :  \mBbbP{}
2.  v  :  Base
3.  v2  :  Base
4.  v  =  v2
5.  v  \mmember{}  Q
6.  v2  \mmember{}  Q
7.  True
8.  v1  :  Base
9.  v3  :  Base
10.  v1  =  v3
11.  v1  \mmember{}  Q
12.  v3  \mmember{}  Q
13.  True
\mvdash{}  v  =  v3


By

---

Latex:
(EqTypeCD  THEN  Auto)

---

Home Index