---

Step * 1 of Lemma not-quotient-true


1. P : ℙ
2. ¬P
3. ⇃(P)
⊢ False
BY
{ TACTIC:((PointwiseFunctionality 3 THEN Auto) THEN EqTypeHD (-1) THEN Auto) }

1
1. P : ℙ
2. ¬P
3. a : Base
4. b : Base
5. c : a = b ∈ pertype(λx,y. ((x ∈ P) ∧ (y ∈ P) ∧ True))
6. a ∈ P
7. b ∈ P
8. True
⊢ False

---

Latex:

---

Latex:

1.  P  :  \mBbbP{}
2.  \mneg{}P
3.  \00D9(P)
\mvdash{}  False


By

---

Latex:
TACTIC:((PointwiseFunctionality  3  THEN  Auto)  THEN  EqTypeHD  (-1)  THEN  Auto)

---

Home Index