Proof of Theorem spr0nelg
| Step | Hyp | Ref
| Expression |
| 1 | | ianor 984 |
. . . . . 6
⊢ (¬
(𝑝 = ∅ ∧
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ (¬ 𝑝 = ∅ ∨ ¬ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
| 2 | 1 | bicomi 224 |
. . . . 5
⊢ ((¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ¬ (𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
| 3 | 2 | albii 1819 |
. . . 4
⊢
(∀𝑝(¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ∀𝑝 ¬ (𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
| 4 | | alnex 1781 |
. . . 4
⊢
(∀𝑝 ¬
(𝑝 = ∅ ∧
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ¬ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
| 5 | 3, 4 | bitri 275 |
. . 3
⊢
(∀𝑝(¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) ↔ ¬ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
| 6 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
| 7 | 6 | prnz 4777 |
. . . . . . . 8
⊢ {𝑎, 𝑏} ≠ ∅ |
| 8 | 7 | nesymi 2998 |
. . . . . . 7
⊢ ¬
∅ = {𝑎, 𝑏} |
| 9 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑝 = ∅ → (𝑝 = {𝑎, 𝑏} ↔ ∅ = {𝑎, 𝑏})) |
| 10 | 8, 9 | mtbiri 327 |
. . . . . 6
⊢ (𝑝 = ∅ → ¬ 𝑝 = {𝑎, 𝑏}) |
| 11 | 10 | alrimivv 1928 |
. . . . 5
⊢ (𝑝 = ∅ → ∀𝑎∀𝑏 ¬ 𝑝 = {𝑎, 𝑏}) |
| 12 | | 2nexaln 1830 |
. . . . 5
⊢ (¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏} ↔ ∀𝑎∀𝑏 ¬ 𝑝 = {𝑎, 𝑏}) |
| 13 | 11, 12 | sylibr 234 |
. . . 4
⊢ (𝑝 = ∅ → ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) |
| 14 | 13 | imori 855 |
. . 3
⊢ (¬
𝑝 = ∅ ∨ ¬
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) |
| 15 | 5, 14 | mpgbi 1798 |
. 2
⊢ ¬
∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}) |
| 16 | | df-nel 3047 |
. . 3
⊢ (∅
∉ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ¬ ∅ ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}) |
| 17 | | clelab 2887 |
. . 3
⊢ (∅
∈ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
| 18 | 16, 17 | xchbinx 334 |
. 2
⊢ (∅
∉ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} ↔ ¬ ∃𝑝(𝑝 = ∅ ∧ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏})) |
| 19 | 15, 18 | mpbir 231 |
1
⊢ ∅
∉ {𝑝 ∣
∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}} |