Step | Hyp | Ref
| Expression |
1 | | 0elpw 3917 |
. . . . 5
⊢ ∅
∈ 𝒫 {𝑧 ∈
{∅} ∣ 𝜑} |
2 | | 0elon 4129 |
. . . . 5
⊢ ∅
∈ On |
3 | | elin 3126 |
. . . . 5
⊢ (∅
∈ (𝒫 {𝑧 ∈
{∅} ∣ 𝜑} ∩
On) ↔ (∅ ∈ 𝒫 {𝑧 ∈ {∅} ∣ 𝜑} ∧ ∅ ∈ On)) |
4 | 1, 2, 3 | mpbir2an 849 |
. . . 4
⊢ ∅
∈ (𝒫 {𝑧 ∈
{∅} ∣ 𝜑} ∩
On) |
5 | | ordtriexmidlem 4245 |
. . . . 5
⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ On |
6 | | suceq 4139 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → suc 𝑥 = suc {𝑧 ∈ {∅} ∣ 𝜑}) |
7 | | pweq 3362 |
. . . . . . . 8
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → 𝒫 𝑥 = 𝒫 {𝑧 ∈ {∅} ∣ 𝜑}) |
8 | 7 | ineq1d 3137 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝒫 𝑥 ∩ On) = (𝒫 {𝑧 ∈ {∅} ∣ 𝜑} ∩ On)) |
9 | 6, 8 | eqeq12d 2054 |
. . . . . 6
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (suc 𝑥 = (𝒫 𝑥 ∩ On) ↔ suc {𝑧 ∈ {∅} ∣ 𝜑} = (𝒫 {𝑧 ∈ {∅} ∣ 𝜑} ∩ On))) |
10 | | ordpwsucexmid.1 |
. . . . . 6
⊢
∀𝑥 ∈ On
suc 𝑥 = (𝒫 𝑥 ∩ On) |
11 | 9, 10 | vtoclri 2628 |
. . . . 5
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ On → suc {𝑧 ∈ {∅} ∣ 𝜑} = (𝒫 {𝑧 ∈ {∅} ∣ 𝜑} ∩ On)) |
12 | 5, 11 | ax-mp 7 |
. . . 4
⊢ suc
{𝑧 ∈ {∅} ∣
𝜑} = (𝒫 {𝑧 ∈ {∅} ∣ 𝜑} ∩ On) |
13 | 4, 12 | eleqtrri 2113 |
. . 3
⊢ ∅
∈ suc {𝑧 ∈
{∅} ∣ 𝜑} |
14 | | elsuci 4140 |
. . 3
⊢ (∅
∈ suc {𝑧 ∈
{∅} ∣ 𝜑} →
(∅ ∈ {𝑧 ∈
{∅} ∣ 𝜑} ∨
∅ = {𝑧 ∈
{∅} ∣ 𝜑})) |
15 | 13, 14 | ax-mp 7 |
. 2
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} ∨ ∅ =
{𝑧 ∈ {∅} ∣
𝜑}) |
16 | | 0ex 3884 |
. . . . . 6
⊢ ∅
∈ V |
17 | 16 | snid 3402 |
. . . . 5
⊢ ∅
∈ {∅} |
18 | | biidd 161 |
. . . . . 6
⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑)) |
19 | 18 | elrab3 2699 |
. . . . 5
⊢ (∅
∈ {∅} → (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑)) |
20 | 17, 19 | ax-mp 7 |
. . . 4
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} ↔ 𝜑) |
21 | 20 | biimpi 113 |
. . 3
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} → 𝜑) |
22 | | ordtriexmidlem2 4246 |
. . . 4
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ → ¬ 𝜑) |
23 | 22 | eqcoms 2043 |
. . 3
⊢ (∅
= {𝑧 ∈ {∅}
∣ 𝜑} → ¬ 𝜑) |
24 | 21, 23 | orim12i 676 |
. 2
⊢ ((∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} ∨ ∅ =
{𝑧 ∈ {∅} ∣
𝜑}) → (𝜑 ∨ ¬ 𝜑)) |
25 | 15, 24 | ax-mp 7 |
1
⊢ (𝜑 ∨ ¬ 𝜑) |