Step | Hyp | Ref
| Expression |
1 | | 0elpw 3908 |
. . . . 5
⊢ ∅
∈ 𝒫 {z ∈ {∅}
∣ φ} |
2 | | 0elon 4095 |
. . . . 5
⊢ ∅
∈ On |
3 | | elin 3120 |
. . . . 5
⊢ (∅
∈ (𝒫 {z ∈ {∅}
∣ φ} ∩ On) ↔ (∅
∈ 𝒫 {z ∈ {∅}
∣ φ} ∧ ∅ ∈
On)) |
4 | 1, 2, 3 | mpbir2an 848 |
. . . 4
⊢ ∅
∈ (𝒫 {z ∈ {∅}
∣ φ} ∩ On) |
5 | | ordtriexmidlem 4208 |
. . . . 5
⊢ {z ∈ {∅}
∣ φ} ∈ On |
6 | | suceq 4105 |
. . . . . . 7
⊢ (x = {z ∈ {∅} ∣ φ} → suc x = suc {z ∈ {∅} ∣ φ}) |
7 | | pweq 3354 |
. . . . . . . 8
⊢ (x = {z ∈ {∅} ∣ φ} → 𝒫 x = 𝒫 {z
∈ {∅} ∣ φ}) |
8 | 7 | ineq1d 3131 |
. . . . . . 7
⊢ (x = {z ∈ {∅} ∣ φ} → (𝒫 x ∩ On) = (𝒫 {z ∈ {∅}
∣ φ} ∩ On)) |
9 | 6, 8 | eqeq12d 2051 |
. . . . . 6
⊢ (x = {z ∈ {∅} ∣ φ} → (suc x = (𝒫 x
∩ On) ↔ suc {z ∈ {∅} ∣ φ} = (𝒫 {z ∈ {∅}
∣ φ} ∩ On))) |
10 | | ordpwsucexmid.1 |
. . . . . 6
⊢ ∀x ∈ On suc x =
(𝒫 x ∩ On) |
11 | 9, 10 | vtoclri 2622 |
. . . . 5
⊢
({z ∈ {∅} ∣ φ} ∈ On
→ suc {z ∈ {∅} ∣ φ} = (𝒫 {z ∈ {∅}
∣ φ} ∩ On)) |
12 | 5, 11 | ax-mp 7 |
. . . 4
⊢ suc
{z ∈
{∅} ∣ φ} = (𝒫
{z ∈
{∅} ∣ φ} ∩
On) |
13 | 4, 12 | eleqtrri 2110 |
. . 3
⊢ ∅
∈ suc {z
∈ {∅} ∣ φ} |
14 | | elsuci 4106 |
. . 3
⊢ (∅
∈ suc {z
∈ {∅} ∣ φ} → (∅ ∈ {z ∈ {∅} ∣ φ} ∨ ∅
= {z ∈
{∅} ∣ φ})) |
15 | 13, 14 | ax-mp 7 |
. 2
⊢ (∅
∈ {z
∈ {∅} ∣ φ} ∨ ∅
= {z ∈
{∅} ∣ φ}) |
16 | | 0ex 3875 |
. . . . . 6
⊢ ∅
∈ V |
17 | 16 | snid 3394 |
. . . . 5
⊢ ∅
∈ {∅} |
18 | | biidd 161 |
. . . . . 6
⊢ (z = ∅ → (φ ↔ φ)) |
19 | 18 | elrab3 2693 |
. . . . 5
⊢ (∅
∈ {∅} → (∅ ∈ {z ∈ {∅} ∣ φ} ↔ φ)) |
20 | 17, 19 | ax-mp 7 |
. . . 4
⊢ (∅
∈ {z
∈ {∅} ∣ φ} ↔ φ) |
21 | 20 | biimpi 113 |
. . 3
⊢ (∅
∈ {z
∈ {∅} ∣ φ} → φ) |
22 | | ordtriexmidlem2 4209 |
. . . 4
⊢
({z ∈ {∅} ∣ φ} = ∅ → ¬ φ) |
23 | 22 | eqcoms 2040 |
. . 3
⊢ (∅
= {z ∈
{∅} ∣ φ} → ¬ φ) |
24 | 21, 23 | orim12i 675 |
. 2
⊢ ((∅
∈ {z
∈ {∅} ∣ φ} ∨ ∅
= {z ∈
{∅} ∣ φ}) → (φ ∨ ¬
φ)) |
25 | 15, 24 | ax-mp 7 |
1
⊢ (φ ∨ ¬
φ) |