Step | Hyp | Ref
| Expression |
1 | | ordtri2or2exmid.1 |
. . . 4
⊢
∀𝑥 ∈ On
∀𝑦 ∈ On (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) |
2 | | ordtri2or2exmidlem 4510 |
. . . . 5
⊢ {𝑧 ∈ {∅, {∅}}
∣ 𝜑} ∈
On |
3 | | suc0 4396 |
. . . . . 6
⊢ suc
∅ = {∅} |
4 | | 0elon 4377 |
. . . . . . 7
⊢ ∅
∈ On |
5 | 4 | onsuci 4500 |
. . . . . 6
⊢ suc
∅ ∈ On |
6 | 3, 5 | eqeltrri 2244 |
. . . . 5
⊢ {∅}
∈ On |
7 | | sseq1 3170 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → (𝑥 ⊆ 𝑦 ↔ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦)) |
8 | | sseq2 3171 |
. . . . . . 7
⊢ (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑})) |
9 | 7, 8 | orbi12d 788 |
. . . . . 6
⊢ (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → ((𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥) ↔ ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦 ∨ 𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}))) |
10 | | sseq2 3171 |
. . . . . . 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 | | elirr 4525 |
. . . . 5
⊢ ¬
{∅} ∈ {∅} |
17 | | simpl 108 |
. . . . . . 7
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → {𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆
{∅}) |
18 | | simpr 109 |
. . . . . . . 8
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → 𝜑) |
19 | | p0ex 4174 |
. . . . . . . . . 10
⊢ {∅}
∈ V |
20 | 19 | prid2 3690 |
. . . . . . . . 9
⊢ {∅}
∈ {∅, {∅}} |
21 | | biidd 171 |
. . . . . . . . . 10
⊢ (𝑧 = {∅} → (𝜑 ↔ 𝜑)) |
22 | 21 | elrab3 2887 |
. . . . . . . . 9
⊢
({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}}
∣ 𝜑} ↔ 𝜑)) |
23 | 20, 22 | ax-mp 5 |
. . . . . . . 8
⊢
({∅} ∈ {𝑧
∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑) |
24 | 18, 23 | sylibr 133 |
. . . . . . 7
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → {∅}
∈ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑}) |
25 | 17, 24 | sseldd 3148 |
. . . . . 6
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∧ 𝜑) → {∅}
∈ {∅}) |
26 | 25 | ex 114 |
. . . . 5
⊢ ({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
→ (𝜑 → {∅}
∈ {∅})) |
27 | 16, 26 | mtoi 659 |
. . . 4
⊢ ({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
→ ¬ 𝜑) |
28 | | snssg 3716 |
. . . . . 6
⊢ (∅
∈ On → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅, {∅}}
∣ 𝜑})) |
29 | 4, 28 | ax-mp 5 |
. . . . 5
⊢ (∅
∈ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑} ↔
{∅} ⊆ {𝑧 ∈
{∅, {∅}} ∣ 𝜑}) |
30 | | 0ex 4116 |
. . . . . . . 8
⊢ ∅
∈ V |
31 | 30 | prid1 3689 |
. . . . . . 7
⊢ ∅
∈ {∅, {∅}} |
32 | | biidd 171 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑)) |
33 | 32 | elrab3 2887 |
. . . . . . 7
⊢ (∅
∈ {∅, {∅}} → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑)) |
34 | 31, 33 | ax-mp 5 |
. . . . . 6
⊢ (∅
∈ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑} ↔
𝜑) |
35 | 34 | biimpi 119 |
. . . . 5
⊢ (∅
∈ {𝑧 ∈ {∅,
{∅}} ∣ 𝜑} →
𝜑) |
36 | 29, 35 | sylbir 134 |
. . . 4
⊢
({∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → 𝜑) |
37 | 27, 36 | orim12i 754 |
. . 3
⊢ (({𝑧 ∈ {∅, {∅}}
∣ 𝜑} ⊆ {∅}
∨ {∅} ⊆ {𝑧
∈ {∅, {∅}} ∣ 𝜑}) → (¬ 𝜑 ∨ 𝜑)) |
38 | 15, 37 | ax-mp 5 |
. 2
⊢ (¬
𝜑 ∨ 𝜑) |
39 | | orcom 723 |
. 2
⊢ ((¬
𝜑 ∨ 𝜑) ↔ (𝜑 ∨ ¬ 𝜑)) |
40 | 38, 39 | mpbi 144 |
1
⊢ (𝜑 ∨ ¬ 𝜑) |