Step | Hyp | Ref
| Expression |
1 | | 0ex 3884 |
. . . . 5
⊢ ∅
∈ V |
2 | | snfig 6291 |
. . . . 5
⊢ (∅
∈ V → {∅} ∈ Fin) |
3 | 1, 2 | ax-mp 7 |
. . . 4
⊢ {∅}
∈ Fin |
4 | | ssrab2 3025 |
. . . 4
⊢ {𝑧 ∈ {∅} ∣ 𝜑} ⊆
{∅} |
5 | | ssfiexmid.1 |
. . . . . 6
⊢
∀𝑥∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin) |
6 | | p0ex 3939 |
. . . . . . 7
⊢ {∅}
∈ V |
7 | | eleq1 2100 |
. . . . . . . . . 10
⊢ (𝑥 = {∅} → (𝑥 ∈ Fin ↔ {∅}
∈ Fin)) |
8 | | sseq2 2967 |
. . . . . . . . . 10
⊢ (𝑥 = {∅} → (𝑦 ⊆ 𝑥 ↔ 𝑦 ⊆ {∅})) |
9 | 7, 8 | anbi12d 442 |
. . . . . . . . 9
⊢ (𝑥 = {∅} → ((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) ↔ ({∅} ∈ Fin ∧ 𝑦 ⊆
{∅}))) |
10 | 9 | imbi1d 220 |
. . . . . . . 8
⊢ (𝑥 = {∅} → (((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin) ↔ (({∅} ∈ Fin
∧ 𝑦 ⊆ {∅})
→ 𝑦 ∈
Fin))) |
11 | 10 | albidv 1705 |
. . . . . . 7
⊢ (𝑥 = {∅} →
(∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin) ↔ ∀𝑦(({∅} ∈ Fin ∧
𝑦 ⊆ {∅}) →
𝑦 ∈
Fin))) |
12 | 6, 11 | spcv 2646 |
. . . . . 6
⊢
(∀𝑥∀𝑦((𝑥 ∈ Fin ∧ 𝑦 ⊆ 𝑥) → 𝑦 ∈ Fin) → ∀𝑦(({∅} ∈ Fin ∧
𝑦 ⊆ {∅}) →
𝑦 ∈
Fin)) |
13 | 5, 12 | ax-mp 7 |
. . . . 5
⊢
∀𝑦(({∅}
∈ Fin ∧ 𝑦 ⊆
{∅}) → 𝑦 ∈
Fin) |
14 | 6 | rabex 3901 |
. . . . . 6
⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ V |
15 | | sseq1 2966 |
. . . . . . . 8
⊢ (𝑦 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑦 ⊆ {∅} ↔ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅})) |
16 | 15 | anbi2d 437 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∈ {∅} ∣ 𝜑} → (({∅} ∈ Fin ∧ 𝑦 ⊆ {∅}) ↔
({∅} ∈ Fin ∧ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}))) |
17 | | eleq1 2100 |
. . . . . . 7
⊢ (𝑦 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑦 ∈ Fin ↔ {𝑧 ∈ {∅} ∣ 𝜑} ∈ Fin)) |
18 | 16, 17 | imbi12d 223 |
. . . . . 6
⊢ (𝑦 = {𝑧 ∈ {∅} ∣ 𝜑} → ((({∅} ∈ Fin ∧ 𝑦 ⊆ {∅}) → 𝑦 ∈ Fin) ↔ (({∅}
∈ Fin ∧ {𝑧 ∈
{∅} ∣ 𝜑} ⊆
{∅}) → {𝑧 ∈
{∅} ∣ 𝜑} ∈
Fin))) |
19 | 14, 18 | spcv 2646 |
. . . . 5
⊢
(∀𝑦(({∅} ∈ Fin ∧ 𝑦 ⊆ {∅}) → 𝑦 ∈ Fin) → (({∅}
∈ Fin ∧ {𝑧 ∈
{∅} ∣ 𝜑} ⊆
{∅}) → {𝑧 ∈
{∅} ∣ 𝜑} ∈
Fin)) |
20 | 13, 19 | ax-mp 7 |
. . . 4
⊢
(({∅} ∈ Fin ∧ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}) → {𝑧 ∈ {∅} ∣ 𝜑} ∈ Fin) |
21 | 3, 4, 20 | mp2an 402 |
. . 3
⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ Fin |
22 | | isfi 6241 |
. . 3
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ∈ Fin ↔ ∃𝑛 ∈ ω {𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛) |
23 | 21, 22 | mpbi 133 |
. 2
⊢
∃𝑛 ∈
ω {𝑧 ∈ {∅}
∣ 𝜑} ≈ 𝑛 |
24 | | 0elnn 4340 |
. . . . 5
⊢ (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∅ ∈
𝑛)) |
25 | | breq2 3768 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → ({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ↔ {𝑧 ∈ {∅} ∣ 𝜑} ≈ ∅)) |
26 | | en0 6275 |
. . . . . . . . . 10
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ≈ ∅ ↔ {𝑧 ∈ {∅} ∣ 𝜑} = ∅) |
27 | 25, 26 | syl6bb 185 |
. . . . . . . . 9
⊢ (𝑛 = ∅ → ({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ↔ {𝑧 ∈ {∅} ∣ 𝜑} = ∅)) |
28 | 27 | biimpac 282 |
. . . . . . . 8
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ∧ 𝑛 = ∅) → {𝑧 ∈ {∅} ∣ 𝜑} = ∅) |
29 | | rabeq0 3247 |
. . . . . . . . 9
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ ↔ ∀𝑧 ∈ {∅} ¬ 𝜑) |
30 | 1 | snm 3488 |
. . . . . . . . . 10
⊢
∃𝑤 𝑤 ∈
{∅} |
31 | | r19.3rmv 3312 |
. . . . . . . . . 10
⊢
(∃𝑤 𝑤 ∈ {∅} → (¬
𝜑 ↔ ∀𝑧 ∈ {∅} ¬ 𝜑)) |
32 | 30, 31 | ax-mp 7 |
. . . . . . . . 9
⊢ (¬
𝜑 ↔ ∀𝑧 ∈ {∅} ¬ 𝜑) |
33 | 29, 32 | bitr4i 176 |
. . . . . . . 8
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} = ∅ ↔ ¬ 𝜑) |
34 | 28, 33 | sylib 127 |
. . . . . . 7
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ∧ 𝑛 = ∅) → ¬ 𝜑) |
35 | 34 | olcd 653 |
. . . . . 6
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ∧ 𝑛 = ∅) → (𝜑 ∨ ¬ 𝜑)) |
36 | | ensym 6261 |
. . . . . . . 8
⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 → 𝑛 ≈ {𝑧 ∈ {∅} ∣ 𝜑}) |
37 | | elex2 2570 |
. . . . . . . 8
⊢ (∅
∈ 𝑛 →
∃𝑥 𝑥 ∈ 𝑛) |
38 | | enm 6294 |
. . . . . . . 8
⊢ ((𝑛 ≈ {𝑧 ∈ {∅} ∣ 𝜑} ∧ ∃𝑥 𝑥 ∈ 𝑛) → ∃𝑦 𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑}) |
39 | 36, 37, 38 | syl2an 273 |
. . . . . . 7
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ∧ ∅ ∈ 𝑛) → ∃𝑦 𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑}) |
40 | | biidd 161 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜑)) |
41 | 40 | elrab 2698 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ (𝑦 ∈ {∅} ∧ 𝜑)) |
42 | 41 | simprbi 260 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑} → 𝜑) |
43 | 42 | orcd 652 |
. . . . . . . 8
⊢ (𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑} → (𝜑 ∨ ¬ 𝜑)) |
44 | 43 | exlimiv 1489 |
. . . . . . 7
⊢
(∃𝑦 𝑦 ∈ {𝑧 ∈ {∅} ∣ 𝜑} → (𝜑 ∨ ¬ 𝜑)) |
45 | 39, 44 | syl 14 |
. . . . . 6
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ∧ ∅ ∈ 𝑛) → (𝜑 ∨ ¬ 𝜑)) |
46 | 35, 45 | jaodan 710 |
. . . . 5
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ∧ (𝑛 = ∅ ∨ ∅ ∈ 𝑛)) → (𝜑 ∨ ¬ 𝜑)) |
47 | 24, 46 | sylan2 270 |
. . . 4
⊢ (({𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛 ∧ 𝑛 ∈ ω) → (𝜑 ∨ ¬ 𝜑)) |
48 | 47 | ancoms 255 |
. . 3
⊢ ((𝑛 ∈ ω ∧ {𝑧 ∈ {∅} ∣ 𝜑} ≈ 𝑛) → (𝜑 ∨ ¬ 𝜑)) |
49 | 48 | rexlimiva 2428 |
. 2
⊢
(∃𝑛 ∈
ω {𝑧 ∈ {∅}
∣ 𝜑} ≈ 𝑛 → (𝜑 ∨ ¬ 𝜑)) |
50 | 23, 49 | ax-mp 7 |
1
⊢ (𝜑 ∨ ¬ 𝜑) |