Step | Hyp | Ref
| Expression |
1 | | ordtri2orexmid.1 |
. . . 4
⊢ ∀x ∈ On ∀y ∈ On (x ∈ y ∨ y ⊆ x) |
2 | | ordtriexmidlem 4208 |
. . . . 5
⊢ {z ∈ {∅}
∣ φ} ∈ On |
3 | | suc0 4114 |
. . . . . 6
⊢ suc
∅ = {∅} |
4 | | 0elon 4095 |
. . . . . . 7
⊢ ∅
∈ On |
5 | 4 | onsuci 4207 |
. . . . . 6
⊢ suc
∅ ∈ On |
6 | 3, 5 | eqeltrri 2108 |
. . . . 5
⊢ {∅}
∈ On |
7 | | eleq1 2097 |
. . . . . . 7
⊢ (x = {z ∈ {∅} ∣ φ} → (x ∈ y ↔ {z
∈ {∅} ∣ φ} ∈
y)) |
8 | | sseq2 2961 |
. . . . . . 7
⊢ (x = {z ∈ {∅} ∣ φ} → (y ⊆ x
↔ y ⊆ {z ∈ {∅}
∣ φ})) |
9 | 7, 8 | orbi12d 706 |
. . . . . 6
⊢ (x = {z ∈ {∅} ∣ φ} → ((x ∈ y ∨ y ⊆ x)
↔ ({z ∈ {∅} ∣ φ} ∈
y ∨
y ⊆ {z ∈ {∅}
∣ φ}))) |
10 | | eleq2 2098 |
. . . . . . 7
⊢ (y = {∅} → ({z ∈ {∅}
∣ φ} ∈ y ↔
{z ∈
{∅} ∣ φ} ∈ {∅})) |
11 | | sseq1 2960 |
. . . . . . 7
⊢ (y = {∅} → (y ⊆ {z
∈ {∅} ∣ φ} ↔ {∅} ⊆ {z ∈ {∅}
∣ φ})) |
12 | 10, 11 | orbi12d 706 |
. . . . . 6
⊢ (y = {∅} → (({z ∈ {∅}
∣ φ} ∈ y ∨ y ⊆
{z ∈
{∅} ∣ φ}) ↔ ({z ∈ {∅}
∣ φ} ∈ {∅} ∨
{∅} ⊆ {z ∈ {∅} ∣ φ}))) |
13 | 9, 12 | rspc2va 2657 |
. . . . 5
⊢
((({z ∈ {∅} ∣ φ} ∈ On
∧ {∅} ∈ On) ∧ ∀x ∈ On ∀y ∈ On (x ∈ y ∨ y ⊆ x))
→ ({z ∈ {∅} ∣ φ} ∈
{∅} ∨ {∅} ⊆ {z ∈ {∅}
∣ φ})) |
14 | 2, 6, 13 | mpanl12 412 |
. . . 4
⊢ (∀x ∈ On ∀y ∈ On (x ∈ y ∨ y ⊆ x)
→ ({z ∈ {∅} ∣ φ} ∈
{∅} ∨ {∅} ⊆ {z ∈ {∅}
∣ φ})) |
15 | 1, 14 | ax-mp 7 |
. . 3
⊢
({z ∈ {∅} ∣ φ} ∈
{∅} ∨ {∅} ⊆ {z ∈ {∅}
∣ φ}) |
16 | | elsni 3391 |
. . . . 5
⊢
({z ∈ {∅} ∣ φ} ∈
{∅} → {z ∈ {∅} ∣ φ} = ∅) |
17 | | ordtriexmidlem2 4209 |
. . . . 5
⊢
({z ∈ {∅} ∣ φ} = ∅ → ¬ φ) |
18 | 16, 17 | syl 14 |
. . . 4
⊢
({z ∈ {∅} ∣ φ} ∈
{∅} → ¬ φ) |
19 | | snssg 3491 |
. . . . . 6
⊢ (∅
∈ On → (∅ ∈ {z ∈ {∅} ∣ φ} ↔ {∅} ⊆ {z ∈ {∅}
∣ φ})) |
20 | 4, 19 | ax-mp 7 |
. . . . 5
⊢ (∅
∈ {z
∈ {∅} ∣ φ} ↔ {∅} ⊆ {z ∈ {∅}
∣ φ}) |
21 | | 0ex 3875 |
. . . . . . . 8
⊢ ∅
∈ V |
22 | 21 | snid 3394 |
. . . . . . 7
⊢ ∅
∈ {∅} |
23 | | biidd 161 |
. . . . . . . 8
⊢ (z = ∅ → (φ ↔ φ)) |
24 | 23 | elrab3 2693 |
. . . . . . 7
⊢ (∅
∈ {∅} → (∅ ∈ {z ∈ {∅} ∣ φ} ↔ φ)) |
25 | 22, 24 | ax-mp 7 |
. . . . . 6
⊢ (∅
∈ {z
∈ {∅} ∣ φ} ↔ φ) |
26 | 25 | biimpi 113 |
. . . . 5
⊢ (∅
∈ {z
∈ {∅} ∣ φ} → φ) |
27 | 20, 26 | sylbir 125 |
. . . 4
⊢
({∅} ⊆ {z ∈ {∅} ∣ φ} → φ) |
28 | 18, 27 | orim12i 675 |
. . 3
⊢
(({z ∈ {∅} ∣ φ} ∈
{∅} ∨ {∅} ⊆ {z ∈ {∅}
∣ φ}) → (¬ φ ∨ φ)) |
29 | 15, 28 | ax-mp 7 |
. 2
⊢ (¬
φ ∨
φ) |
30 | | orcom 646 |
. 2
⊢ ((¬
φ ∨
φ) ↔ (φ ∨ ¬
φ)) |
31 | 29, 30 | mpbi 133 |
1
⊢ (φ ∨ ¬
φ) |