Step | Hyp | Ref
| Expression |
1 | | ordtri2orexmid.1 |
. . . 4
⊢
∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑦 ⊆ 𝑥) |
2 | | ordtriexmidlem 4501 |
. . . . 5
⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ On |
3 | | suc0 4394 |
. . . . . 6
⊢ suc
∅ = {∅} |
4 | | 0elon 4375 |
. . . . . . 7
⊢ ∅
∈ On |
5 | 4 | onsuci 4498 |
. . . . . 6
⊢ suc
∅ ∈ On |
6 | 3, 5 | eqeltrri 2244 |
. . . . 5
⊢ {∅}
∈ On |
7 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦)) |
8 | | sseq2 3171 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ {𝑧 ∈ {∅} ∣ 𝜑})) |
9 | 7, 8 | orbi12d 788 |
. . . . . 6
⊢ (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ 𝑦 ∨ 𝑦 ⊆ 𝑥) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦 ∨ 𝑦 ⊆ {𝑧 ∈ {∅} ∣ 𝜑}))) |
10 | | eleq2 2234 |
. . . . . . 7
⊢ (𝑦 = {∅} → ({𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅})) |
11 | | sseq1 3170 |
. . . . . . 7
⊢ (𝑦 = {∅} → (𝑦 ⊆ {𝑧 ∈ {∅} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅} ∣ 𝜑})) |
12 | 10, 11 | orbi12d 788 |
. . . . . 6
⊢ (𝑦 = {∅} → (({𝑧 ∈ {∅} ∣ 𝜑} ∈ 𝑦 ∨ 𝑦 ⊆ {𝑧 ∈ {∅} ∣ 𝜑}) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅} ⊆
{𝑧 ∈ {∅} ∣
𝜑}))) |
13 | 9, 12 | rspc2va 2848 |
. . . . 5
⊢ ((({𝑧 ∈ {∅} ∣ 𝜑} ∈ On ∧ {∅} ∈
On) ∧ ∀𝑥 ∈
On ∀𝑦 ∈ On
(𝑥 ∈ 𝑦 ∨ 𝑦 ⊆ 𝑥)) → ({𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅} ⊆
{𝑧 ∈ {∅} ∣
𝜑})) |
14 | 2, 6, 13 | mpanl12 434 |
. . . 4
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ∈ 𝑦 ∨ 𝑦 ⊆ 𝑥) → ({𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅} ⊆
{𝑧 ∈ {∅} ∣
𝜑})) |
15 | 1, 14 | ax-mp 5 |
. . 3
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅}
⊆ {𝑧 ∈ {∅}
∣ 𝜑}) |
16 | | elsni 3599 |
. . . . 5
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅} → {𝑧 ∈ {∅} ∣ 𝜑} = ∅) |
17 | | ordtriexmidlem2 4502 |
. . . . 5
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ → ¬ 𝜑) |
18 | 16, 17 | syl 14 |
. . . 4
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅} → ¬
𝜑) |
19 | | snssg 3714 |
. . . . . 6
⊢ (∅
∈ On → (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅} ∣ 𝜑})) |
20 | 4, 19 | ax-mp 5 |
. . . . 5
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} ↔ {∅}
⊆ {𝑧 ∈ {∅}
∣ 𝜑}) |
21 | | 0ex 4114 |
. . . . . . . 8
⊢ ∅
∈ V |
22 | 21 | snid 3612 |
. . . . . . 7
⊢ ∅
∈ {∅} |
23 | | biidd 171 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑)) |
24 | 23 | elrab3 2887 |
. . . . . . 7
⊢ (∅
∈ {∅} → (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑)) |
25 | 22, 24 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} ↔ 𝜑) |
26 | 25 | biimpi 119 |
. . . . 5
⊢ (∅
∈ {𝑧 ∈ {∅}
∣ 𝜑} → 𝜑) |
27 | 20, 26 | sylbir 134 |
. . . 4
⊢
({∅} ⊆ {𝑧 ∈ {∅} ∣ 𝜑} → 𝜑) |
28 | 18, 27 | orim12i 754 |
. . 3
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅}
⊆ {𝑧 ∈ {∅}
∣ 𝜑}) → (¬
𝜑 ∨ 𝜑)) |
29 | 15, 28 | ax-mp 5 |
. 2
⊢ (¬
𝜑 ∨ 𝜑) |
30 | | orcom 723 |
. 2
⊢ ((¬
𝜑 ∨ 𝜑) ↔ (𝜑 ∨ ¬ 𝜑)) |
31 | 29, 30 | mpbi 144 |
1
⊢ (𝜑 ∨ ¬ 𝜑) |