Proof of Theorem spr0nelg
Step | Hyp | Ref
| Expression |
1 | | ianor 978 |
. . . . . 6
⊢ (¬
(𝑝 = ∅ ∧
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ (¬ 𝑝 = ∅ ∨ ¬ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
2 | 1 | bicomi 223 |
. . . . 5
⊢ ((¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ¬ (𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
3 | 2 | albii 1825 |
. . . 4
⊢
(∀𝑝(¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ∀𝑝 ¬ (𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
4 | | alnex 1787 |
. . . 4
⊢
(∀𝑝 ¬
(𝑝 = ∅ ∧
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ¬ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
5 | 3, 4 | bitri 274 |
. . 3
⊢
(∀𝑝(¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ¬ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
6 | | vex 3434 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
7 | 6 | prnz 4718 |
. . . . . . . 8
⊢ {𝑎, 𝑏} ≠ ∅ |
8 | 7 | nesymi 3002 |
. . . . . . 7
⊢ ¬
∅ = {𝑎, 𝑏} |
9 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑝 = ∅ → (𝑝 = {𝑎, 𝑏} ↔ ∅ = {𝑎, 𝑏})) |
10 | 8, 9 | mtbiri 326 |
. . . . . 6
⊢ (𝑝 = ∅ → ¬ 𝑝 = {𝑎, 𝑏}) |
11 | 10 | alrimivv 1934 |
. . . . 5
⊢ (𝑝 = ∅ → ∀𝑎∀𝑏 ¬ 𝑝 = {𝑎, 𝑏}) |
12 | | 2nexaln 1835 |
. . . . 5
⊢ (¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏} ↔ ∀𝑎∀𝑏 ¬ 𝑝 = {𝑎, 𝑏}) |
13 | 11, 12 | sylibr 233 |
. . . 4
⊢ (𝑝 = ∅ → ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) |
14 | 13 | imori 850 |
. . 3
⊢ (¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) |
15 | 5, 14 | mpgbi 1804 |
. 2
⊢ ¬
∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) |
16 | | df-nel 3051 |
. . 3
⊢ (∅
∉ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ¬ ∅ ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}) |
17 | | clelab 2884 |
. . 3
⊢ (∅
∈ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
18 | 16, 17 | xchbinx 333 |
. 2
⊢ (∅
∉ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ¬ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
19 | 15, 18 | mpbir 230 |
1
⊢ ∅
∉ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} |