Step | Hyp | Ref
| Expression |
1 | | ordtriexmidlem 4503 |
. . . . 5
⊢ {𝑤 ∈ {∅} ∣ 𝜑} ∈ On |
2 | 1 | elexi 2742 |
. . . 4
⊢ {𝑤 ∈ {∅} ∣ 𝜑} ∈ V |
3 | 2 | sucid 4402 |
. . 3
⊢ {𝑤 ∈ {∅} ∣ 𝜑} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} |
4 | 1 | onsuci 4500 |
. . . 4
⊢ suc
{𝑤 ∈ {∅} ∣
𝜑} ∈ On |
5 | | suc0 4396 |
. . . . 5
⊢ suc
∅ = {∅} |
6 | | 0elon 4377 |
. . . . . 6
⊢ ∅
∈ On |
7 | 6 | onsuci 4500 |
. . . . 5
⊢ suc
∅ ∈ On |
8 | 5, 7 | eqeltrri 2244 |
. . . 4
⊢ {∅}
∈ On |
9 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑥 = {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ On ↔ {𝑤 ∈ {∅} ∣ 𝜑} ∈ On)) |
10 | 9 | 3anbi1d 1311 |
. . . . . 6
⊢ (𝑥 = {𝑤 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ On ∧ suc {𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ {∅} ∈ On)
↔ ({𝑤 ∈ {∅}
∣ 𝜑} ∈ On ∧
suc {𝑤 ∈ {∅}
∣ 𝜑} ∈ On ∧
{∅} ∈ On))) |
11 | | eleq1 2233 |
. . . . . . 7
⊢ (𝑥 = {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} ↔ {𝑤 ∈ {∅} ∣ 𝜑} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑})) |
12 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑥 = {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ {∅} ↔ {𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅})) |
13 | 12 | orbi1d 786 |
. . . . . . 7
⊢ (𝑥 = {𝑤 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑}) ↔ ({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅}
∈ suc {𝑤 ∈
{∅} ∣ 𝜑}))) |
14 | 11, 13 | imbi12d 233 |
. . . . . 6
⊢ (𝑥 = {𝑤 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑})) ↔ ({𝑤 ∈ {∅} ∣ 𝜑} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → ({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑})))) |
15 | 10, 14 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = {𝑤 ∈ {∅} ∣ 𝜑} → (((𝑥 ∈ On ∧ suc {𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ {∅} ∈ On)
→ (𝑥 ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑}))) ↔ (({𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ suc {𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ {∅} ∈
On) → ({𝑤 ∈
{∅} ∣ 𝜑} ∈
suc {𝑤 ∈ {∅}
∣ 𝜑} → ({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅}
∈ suc {𝑤 ∈
{∅} ∣ 𝜑}))))) |
16 | 4 | elexi 2742 |
. . . . . 6
⊢ suc
{𝑤 ∈ {∅} ∣
𝜑} ∈ V |
17 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑦 = suc {𝑤 ∈ {∅} ∣ 𝜑} → (𝑦 ∈ On ↔ suc {𝑤 ∈ {∅} ∣ 𝜑} ∈ On)) |
18 | 17 | 3anbi2d 1312 |
. . . . . . 7
⊢ (𝑦 = suc {𝑤 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ {∅} ∈ On) ↔
(𝑥 ∈ On ∧ suc
{𝑤 ∈ {∅} ∣
𝜑} ∈ On ∧ {∅}
∈ On))) |
19 | | eleq2 2234 |
. . . . . . . 8
⊢ (𝑦 = suc {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ suc {𝑤 ∈ {∅} ∣ 𝜑})) |
20 | | eleq2 2234 |
. . . . . . . . 9
⊢ (𝑦 = suc {𝑤 ∈ {∅} ∣ 𝜑} → ({∅} ∈ 𝑦 ↔ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑})) |
21 | 20 | orbi2d 785 |
. . . . . . . 8
⊢ (𝑦 = suc {𝑤 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ {∅} ∨ {∅} ∈ 𝑦) ↔ (𝑥 ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑}))) |
22 | 19, 21 | imbi12d 233 |
. . . . . . 7
⊢ (𝑦 = suc {𝑤 ∈ {∅} ∣ 𝜑} → ((𝑥 ∈ 𝑦 → (𝑥 ∈ {∅} ∨ {∅} ∈ 𝑦)) ↔ (𝑥 ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑})))) |
23 | 18, 22 | imbi12d 233 |
. . . . . 6
⊢ (𝑦 = suc {𝑤 ∈ {∅} ∣ 𝜑} → (((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ {∅} ∈ On) →
(𝑥 ∈ 𝑦 → (𝑥 ∈ {∅} ∨ {∅} ∈ 𝑦))) ↔ ((𝑥 ∈ On ∧ suc {𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ {∅} ∈ On)
→ (𝑥 ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → (𝑥 ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑}))))) |
24 | | p0ex 4174 |
. . . . . . 7
⊢ {∅}
∈ V |
25 | | eleq1 2233 |
. . . . . . . . 9
⊢ (𝑧 = {∅} → (𝑧 ∈ On ↔ {∅}
∈ On)) |
26 | 25 | 3anbi3d 1313 |
. . . . . . . 8
⊢ (𝑧 = {∅} → ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑧 ∈ On) ↔ (𝑥 ∈ On ∧ 𝑦 ∈ On ∧ {∅}
∈ On))) |
27 | | eleq2 2234 |
. . . . . . . . . 10
⊢ (𝑧 = {∅} → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ {∅})) |
28 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑧 = {∅} → (𝑧 ∈ 𝑦 ↔ {∅} ∈ 𝑦)) |
29 | 27, 28 | orbi12d 788 |
. . . . . . . . 9
⊢ (𝑧 = {∅} → ((𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦) ↔ (𝑥 ∈ {∅} ∨ {∅} ∈ 𝑦))) |
30 | 29 | imbi2d 229 |
. . . . . . . 8
⊢ (𝑧 = {∅} → ((𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦)) ↔ (𝑥 ∈ 𝑦 → (𝑥 ∈ {∅} ∨ {∅} ∈ 𝑦)))) |
31 | 26, 30 | imbi12d 233 |
. . . . . . 7
⊢ (𝑧 = {∅} → (((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑧 ∈ On) → (𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦))) ↔ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ {∅} ∈ On) →
(𝑥 ∈ 𝑦 → (𝑥 ∈ {∅} ∨ {∅} ∈ 𝑦))))) |
32 | | ordsoexmid.1 |
. . . . . . . . . . 11
⊢ E Or
On |
33 | | df-iso 4282 |
. . . . . . . . . . 11
⊢ ( E Or On
↔ ( E Po On ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑥 E 𝑦 → (𝑥 E 𝑧 ∨ 𝑧 E 𝑦)))) |
34 | 32, 33 | mpbi 144 |
. . . . . . . . . 10
⊢ ( E Po On
∧ ∀𝑥 ∈ On
∀𝑦 ∈ On
∀𝑧 ∈ On (𝑥 E 𝑦 → (𝑥 E 𝑧 ∨ 𝑧 E 𝑦))) |
35 | 34 | simpri 112 |
. . . . . . . . 9
⊢
∀𝑥 ∈ On
∀𝑦 ∈ On
∀𝑧 ∈ On (𝑥 E 𝑦 → (𝑥 E 𝑧 ∨ 𝑧 E 𝑦)) |
36 | | epel 4277 |
. . . . . . . . . . . 12
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
37 | | epel 4277 |
. . . . . . . . . . . . 13
⊢ (𝑥 E 𝑧 ↔ 𝑥 ∈ 𝑧) |
38 | | epel 4277 |
. . . . . . . . . . . . 13
⊢ (𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦) |
39 | 37, 38 | orbi12i 759 |
. . . . . . . . . . . 12
⊢ ((𝑥 E 𝑧 ∨ 𝑧 E 𝑦) ↔ (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦)) |
40 | 36, 39 | imbi12i 238 |
. . . . . . . . . . 11
⊢ ((𝑥 E 𝑦 → (𝑥 E 𝑧 ∨ 𝑧 E 𝑦)) ↔ (𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦))) |
41 | 40 | 2ralbii 2478 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈ On
∀𝑧 ∈ On (𝑥 E 𝑦 → (𝑥 E 𝑧 ∨ 𝑧 E 𝑦)) ↔ ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦))) |
42 | 41 | ralbii 2476 |
. . . . . . . . 9
⊢
(∀𝑥 ∈ On
∀𝑦 ∈ On
∀𝑧 ∈ On (𝑥 E 𝑦 → (𝑥 E 𝑧 ∨ 𝑧 E 𝑦)) ↔ ∀𝑥 ∈ On ∀𝑦 ∈ On ∀𝑧 ∈ On (𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦))) |
43 | 35, 42 | mpbi 144 |
. . . . . . . 8
⊢
∀𝑥 ∈ On
∀𝑦 ∈ On
∀𝑧 ∈ On (𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦)) |
44 | 43 | rspec3 2560 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑧 ∈ On) → (𝑥 ∈ 𝑦 → (𝑥 ∈ 𝑧 ∨ 𝑧 ∈ 𝑦))) |
45 | 24, 31, 44 | vtocl 2784 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ {∅}
∈ On) → (𝑥 ∈
𝑦 → (𝑥 ∈ {∅} ∨ {∅}
∈ 𝑦))) |
46 | 16, 23, 45 | vtocl 2784 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ suc {𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ {∅} ∈
On) → (𝑥 ∈ suc
{𝑤 ∈ {∅} ∣
𝜑} → (𝑥 ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑}))) |
47 | 2, 15, 46 | vtocl 2784 |
. . . 4
⊢ (({𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ suc {𝑤 ∈ {∅} ∣ 𝜑} ∈ On ∧ {∅} ∈
On) → ({𝑤 ∈
{∅} ∣ 𝜑} ∈
suc {𝑤 ∈ {∅}
∣ 𝜑} → ({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅}
∈ suc {𝑤 ∈
{∅} ∣ 𝜑}))) |
48 | 1, 4, 8, 47 | mp3an 1332 |
. . 3
⊢ ({𝑤 ∈ {∅} ∣ 𝜑} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → ({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅} ∈ suc
{𝑤 ∈ {∅} ∣
𝜑})) |
49 | 2 | elsn 3599 |
. . . . 5
⊢ ({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} ↔ {𝑤 ∈ {∅} ∣ 𝜑} = ∅) |
50 | | ordtriexmidlem2 4504 |
. . . . 5
⊢ ({𝑤 ∈ {∅} ∣ 𝜑} = ∅ → ¬ 𝜑) |
51 | 49, 50 | sylbi 120 |
. . . 4
⊢ ({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} → ¬
𝜑) |
52 | | elirr 4525 |
. . . . . . 7
⊢ ¬
{∅} ∈ {∅} |
53 | | elrabi 2883 |
. . . . . . 7
⊢
({∅} ∈ {𝑤
∈ {∅} ∣ 𝜑}
→ {∅} ∈ {∅}) |
54 | 52, 53 | mto 657 |
. . . . . 6
⊢ ¬
{∅} ∈ {𝑤 ∈
{∅} ∣ 𝜑} |
55 | | elsuci 4388 |
. . . . . . 7
⊢
({∅} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → ({∅} ∈ {𝑤 ∈ {∅} ∣ 𝜑} ∨ {∅} = {𝑤 ∈ {∅} ∣ 𝜑})) |
56 | 55 | ord 719 |
. . . . . 6
⊢
({∅} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → (¬ {∅} ∈ {𝑤 ∈ {∅} ∣ 𝜑} → {∅} = {𝑤 ∈ {∅} ∣ 𝜑})) |
57 | 54, 56 | mpi 15 |
. . . . 5
⊢
({∅} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → {∅} = {𝑤 ∈ {∅} ∣ 𝜑}) |
58 | | 0ex 4116 |
. . . . . . 7
⊢ ∅
∈ V |
59 | | biidd 171 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝜑 ↔ 𝜑)) |
60 | 58, 59 | rabsnt 3658 |
. . . . . 6
⊢ ({𝑤 ∈ {∅} ∣ 𝜑} = {∅} → 𝜑) |
61 | 60 | eqcoms 2173 |
. . . . 5
⊢
({∅} = {𝑤
∈ {∅} ∣ 𝜑}
→ 𝜑) |
62 | 57, 61 | syl 14 |
. . . 4
⊢
({∅} ∈ suc {𝑤 ∈ {∅} ∣ 𝜑} → 𝜑) |
63 | 51, 62 | orim12i 754 |
. . 3
⊢ (({𝑤 ∈ {∅} ∣ 𝜑} ∈ {∅} ∨ {∅}
∈ suc {𝑤 ∈
{∅} ∣ 𝜑}) →
(¬ 𝜑 ∨ 𝜑)) |
64 | 3, 48, 63 | mp2b 8 |
. 2
⊢ (¬
𝜑 ∨ 𝜑) |
65 | | orcom 723 |
. 2
⊢ ((¬
𝜑 ∨ 𝜑) ↔ (𝜑 ∨ ¬ 𝜑)) |
66 | 64, 65 | mpbi 144 |
1
⊢ (𝜑 ∨ ¬ 𝜑) |