Step | Hyp | Ref
| Expression |
1 | | df-pr 3588 |
. . . . 5
⊢ {{𝑧 ∈ 1o ∣
𝜑}, 1o} = ({{𝑧 ∈ 1o ∣
𝜑}} ∪
{1o}) |
2 | | unfiexmid.1 |
. . . . . . 7
⊢ ((𝑥 ∈ Fin ∧ 𝑦 ∈ Fin) → (𝑥 ∪ 𝑦) ∈ Fin) |
3 | 2 | rgen2a 2524 |
. . . . . 6
⊢
∀𝑥 ∈ Fin
∀𝑦 ∈ Fin (𝑥 ∪ 𝑦) ∈ Fin |
4 | | df1o2 6405 |
. . . . . . . . . 10
⊢
1o = {∅} |
5 | | rabeq 2722 |
. . . . . . . . . 10
⊢
(1o = {∅} → {𝑧 ∈ 1o ∣ 𝜑} = {𝑧 ∈ {∅} ∣ 𝜑}) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . 9
⊢ {𝑧 ∈ 1o ∣
𝜑} = {𝑧 ∈ {∅} ∣ 𝜑} |
7 | | ordtriexmidlem 4501 |
. . . . . . . . 9
⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ On |
8 | 6, 7 | eqeltri 2243 |
. . . . . . . 8
⊢ {𝑧 ∈ 1o ∣
𝜑} ∈ On |
9 | | snfig 6788 |
. . . . . . . 8
⊢ ({𝑧 ∈ 1o ∣
𝜑} ∈ On → {{𝑧 ∈ 1o ∣
𝜑}} ∈
Fin) |
10 | 8, 9 | ax-mp 5 |
. . . . . . 7
⊢ {{𝑧 ∈ 1o ∣
𝜑}} ∈
Fin |
11 | | 1onn 6496 |
. . . . . . . 8
⊢
1o ∈ ω |
12 | | snfig 6788 |
. . . . . . . 8
⊢
(1o ∈ ω → {1o} ∈
Fin) |
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
⊢
{1o} ∈ Fin |
14 | | uneq1 3274 |
. . . . . . . . 9
⊢ (𝑥 = {{𝑧 ∈ 1o ∣ 𝜑}} → (𝑥 ∪ 𝑦) = ({{𝑧 ∈ 1o ∣ 𝜑}} ∪ 𝑦)) |
15 | 14 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑥 = {{𝑧 ∈ 1o ∣ 𝜑}} → ((𝑥 ∪ 𝑦) ∈ Fin ↔ ({{𝑧 ∈ 1o ∣ 𝜑}} ∪ 𝑦) ∈ Fin)) |
16 | | uneq2 3275 |
. . . . . . . . 9
⊢ (𝑦 = {1o} →
({{𝑧 ∈ 1o
∣ 𝜑}} ∪ 𝑦) = ({{𝑧 ∈ 1o ∣ 𝜑}} ∪ {1o})) |
17 | 16 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑦 = {1o} →
(({{𝑧 ∈ 1o
∣ 𝜑}} ∪ 𝑦) ∈ Fin ↔ ({{𝑧 ∈ 1o ∣
𝜑}} ∪ {1o})
∈ Fin)) |
18 | 15, 17 | rspc2v 2847 |
. . . . . . 7
⊢ (({{𝑧 ∈ 1o ∣
𝜑}} ∈ Fin ∧
{1o} ∈ Fin) → (∀𝑥 ∈ Fin ∀𝑦 ∈ Fin (𝑥 ∪ 𝑦) ∈ Fin → ({{𝑧 ∈ 1o ∣ 𝜑}} ∪ {1o}) ∈
Fin)) |
19 | 10, 13, 18 | mp2an 424 |
. . . . . 6
⊢
(∀𝑥 ∈
Fin ∀𝑦 ∈ Fin
(𝑥 ∪ 𝑦) ∈ Fin → ({{𝑧 ∈ 1o ∣ 𝜑}} ∪ {1o}) ∈
Fin) |
20 | 3, 19 | ax-mp 5 |
. . . . 5
⊢ ({{𝑧 ∈ 1o ∣
𝜑}} ∪ {1o})
∈ Fin |
21 | 1, 20 | eqeltri 2243 |
. . . 4
⊢ {{𝑧 ∈ 1o ∣
𝜑}, 1o} ∈
Fin |
22 | 8 | elexi 2742 |
. . . . 5
⊢ {𝑧 ∈ 1o ∣
𝜑} ∈ V |
23 | 22 | prid1 3687 |
. . . 4
⊢ {𝑧 ∈ 1o ∣
𝜑} ∈ {{𝑧 ∈ 1o ∣
𝜑},
1o} |
24 | 11 | elexi 2742 |
. . . . 5
⊢
1o ∈ V |
25 | 24 | prid2 3688 |
. . . 4
⊢
1o ∈ {{𝑧 ∈ 1o ∣ 𝜑}, 1o} |
26 | | fidceq 6843 |
. . . 4
⊢ (({{𝑧 ∈ 1o ∣
𝜑}, 1o} ∈ Fin
∧ {𝑧 ∈
1o ∣ 𝜑}
∈ {{𝑧 ∈
1o ∣ 𝜑},
1o} ∧ 1o ∈ {{𝑧 ∈ 1o ∣ 𝜑}, 1o}) →
DECID {𝑧
∈ 1o ∣ 𝜑} = 1o) |
27 | 21, 23, 25, 26 | mp3an 1332 |
. . 3
⊢
DECID {𝑧 ∈ 1o ∣ 𝜑} = 1o |
28 | | exmiddc 831 |
. . 3
⊢
(DECID {𝑧 ∈ 1o ∣ 𝜑} = 1o → ({𝑧 ∈ 1o ∣
𝜑} = 1o ∨ ¬
{𝑧 ∈ 1o
∣ 𝜑} =
1o)) |
29 | 27, 28 | ax-mp 5 |
. 2
⊢ ({𝑧 ∈ 1o ∣
𝜑} = 1o ∨ ¬
{𝑧 ∈ 1o
∣ 𝜑} =
1o) |
30 | 4 | eqeq2i 2181 |
. . . 4
⊢ ({𝑧 ∈ 1o ∣
𝜑} = 1o ↔
{𝑧 ∈ 1o
∣ 𝜑} =
{∅}) |
31 | | 0ex 4114 |
. . . . 5
⊢ ∅
∈ V |
32 | | biidd 171 |
. . . . 5
⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑)) |
33 | 31, 32 | rabsnt 3656 |
. . . 4
⊢ ({𝑧 ∈ 1o ∣
𝜑} = {∅} → 𝜑) |
34 | 30, 33 | sylbi 120 |
. . 3
⊢ ({𝑧 ∈ 1o ∣
𝜑} = 1o →
𝜑) |
35 | | df-rab 2457 |
. . . . 5
⊢ {𝑧 ∈ 1o ∣
𝜑} = {𝑧 ∣ (𝑧 ∈ 1o ∧ 𝜑)} |
36 | | iba 298 |
. . . . . 6
⊢ (𝜑 → (𝑧 ∈ 1o ↔ (𝑧 ∈ 1o ∧
𝜑))) |
37 | 36 | abbi2dv 2289 |
. . . . 5
⊢ (𝜑 → 1o = {𝑧 ∣ (𝑧 ∈ 1o ∧ 𝜑)}) |
38 | 35, 37 | eqtr4id 2222 |
. . . 4
⊢ (𝜑 → {𝑧 ∈ 1o ∣ 𝜑} = 1o) |
39 | 38 | con3i 627 |
. . 3
⊢ (¬
{𝑧 ∈ 1o
∣ 𝜑} = 1o
→ ¬ 𝜑) |
40 | 34, 39 | orim12i 754 |
. 2
⊢ (({𝑧 ∈ 1o ∣
𝜑} = 1o ∨ ¬
{𝑧 ∈ 1o
∣ 𝜑} = 1o)
→ (𝜑 ∨ ¬ 𝜑)) |
41 | 29, 40 | ax-mp 5 |
1
⊢ (𝜑 ∨ ¬ 𝜑) |