Step | Hyp | Ref
| Expression |
1 | | 0ex 4116 |
. . . . . 6
⊢ ∅
∈ V |
2 | | snfig 6792 |
. . . . . 6
⊢ (∅
∈ V → {∅} ∈ Fin) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ {∅}
∈ Fin |
4 | | diffitest.1 |
. . . . 5
⊢
∀𝑎 ∈ Fin
∀𝑏(𝑎 ∖ 𝑏) ∈ Fin |
5 | | difeq1 3238 |
. . . . . . . 8
⊢ (𝑎 = {∅} → (𝑎 ∖ 𝑏) = ({∅} ∖ 𝑏)) |
6 | 5 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑎 = {∅} → ((𝑎 ∖ 𝑏) ∈ Fin ↔ ({∅} ∖ 𝑏) ∈ Fin)) |
7 | 6 | albidv 1817 |
. . . . . 6
⊢ (𝑎 = {∅} →
(∀𝑏(𝑎 ∖ 𝑏) ∈ Fin ↔ ∀𝑏({∅} ∖ 𝑏) ∈ Fin)) |
8 | 7 | rspcv 2830 |
. . . . 5
⊢
({∅} ∈ Fin → (∀𝑎 ∈ Fin ∀𝑏(𝑎 ∖ 𝑏) ∈ Fin → ∀𝑏({∅} ∖ 𝑏) ∈ Fin)) |
9 | 3, 4, 8 | mp2 16 |
. . . 4
⊢
∀𝑏({∅}
∖ 𝑏) ∈
Fin |
10 | | rabexg 4132 |
. . . . . 6
⊢
({∅} ∈ Fin → {𝑥 ∈ {∅} ∣ 𝜑} ∈ V) |
11 | 3, 10 | ax-mp 5 |
. . . . 5
⊢ {𝑥 ∈ {∅} ∣ 𝜑} ∈ V |
12 | | difeq2 3239 |
. . . . . 6
⊢ (𝑏 = {𝑥 ∈ {∅} ∣ 𝜑} → ({∅} ∖ 𝑏) = ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑})) |
13 | 12 | eleq1d 2239 |
. . . . 5
⊢ (𝑏 = {𝑥 ∈ {∅} ∣ 𝜑} → (({∅} ∖ 𝑏) ∈ Fin ↔ ({∅}
∖ {𝑥 ∈ {∅}
∣ 𝜑}) ∈
Fin)) |
14 | 11, 13 | spcv 2824 |
. . . 4
⊢
(∀𝑏({∅}
∖ 𝑏) ∈ Fin
→ ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ∈ Fin) |
15 | 9, 14 | ax-mp 5 |
. . 3
⊢
({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ∈ Fin |
16 | | isfi 6739 |
. . 3
⊢
(({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ∈ Fin ↔ ∃𝑛 ∈ ω ({∅}
∖ {𝑥 ∈ {∅}
∣ 𝜑}) ≈ 𝑛) |
17 | 15, 16 | mpbi 144 |
. 2
⊢
∃𝑛 ∈
ω ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 |
18 | | 0elnn 4603 |
. . . . 5
⊢ (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∅ ∈
𝑛)) |
19 | | breq2 3993 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → (({∅}
∖ {𝑥 ∈ {∅}
∣ 𝜑}) ≈ 𝑛 ↔ ({∅} ∖
{𝑥 ∈ {∅} ∣
𝜑}) ≈
∅)) |
20 | | en0 6773 |
. . . . . . . . . 10
⊢
(({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ ∅ ↔ ({∅} ∖
{𝑥 ∈ {∅} ∣
𝜑}) =
∅) |
21 | 19, 20 | bitrdi 195 |
. . . . . . . . 9
⊢ (𝑛 = ∅ → (({∅}
∖ {𝑥 ∈ {∅}
∣ 𝜑}) ≈ 𝑛 ↔ ({∅} ∖
{𝑥 ∈ {∅} ∣
𝜑}) =
∅)) |
22 | 21 | biimpac 296 |
. . . . . . . 8
⊢
((({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 ∧ 𝑛 = ∅) → ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) = ∅) |
23 | | rabeq0 3444 |
. . . . . . . . 9
⊢ ({𝑥 ∈ {∅} ∣ ¬
𝜑} = ∅ ↔
∀𝑥 ∈ {∅}
¬ ¬ 𝜑) |
24 | | notrab 3404 |
. . . . . . . . . 10
⊢
({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) = {𝑥 ∈ {∅} ∣ ¬ 𝜑} |
25 | 24 | eqeq1i 2178 |
. . . . . . . . 9
⊢
(({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) = ∅ ↔ {𝑥 ∈ {∅} ∣ ¬ 𝜑} = ∅) |
26 | 1 | snm 3703 |
. . . . . . . . . 10
⊢
∃𝑤 𝑤 ∈
{∅} |
27 | | r19.3rmv 3505 |
. . . . . . . . . 10
⊢
(∃𝑤 𝑤 ∈ {∅} → (¬
¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬
𝜑)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . 9
⊢ (¬
¬ 𝜑 ↔ ∀𝑥 ∈ {∅} ¬ ¬
𝜑) |
29 | 23, 25, 28 | 3bitr4i 211 |
. . . . . . . 8
⊢
(({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) = ∅ ↔ ¬ ¬ 𝜑) |
30 | 22, 29 | sylib 121 |
. . . . . . 7
⊢
((({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 ∧ 𝑛 = ∅) → ¬ ¬ 𝜑) |
31 | 30 | olcd 729 |
. . . . . 6
⊢
((({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 ∧ 𝑛 = ∅) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
32 | | ensym 6759 |
. . . . . . . 8
⊢
(({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 → 𝑛 ≈ ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑})) |
33 | | elex2 2746 |
. . . . . . . 8
⊢ (∅
∈ 𝑛 →
∃𝑤 𝑤 ∈ 𝑛) |
34 | | enm 6798 |
. . . . . . . 8
⊢ ((𝑛 ≈ ({∅} ∖
{𝑥 ∈ {∅} ∣
𝜑}) ∧ ∃𝑤 𝑤 ∈ 𝑛) → ∃𝑦 𝑦 ∈ ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑})) |
35 | 32, 33, 34 | syl2an 287 |
. . . . . . 7
⊢
((({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 ∧ ∅ ∈ 𝑛) → ∃𝑦 𝑦 ∈ ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑})) |
36 | | biidd 171 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (¬ 𝜑 ↔ ¬ 𝜑)) |
37 | 36 | elrab 2886 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} ↔ (𝑦 ∈ {∅} ∧ ¬ 𝜑)) |
38 | 37 | simprbi 273 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → ¬ 𝜑) |
39 | 38 | orcd 728 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑥 ∈ {∅} ∣ ¬ 𝜑} → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
40 | 39, 24 | eleq2s 2265 |
. . . . . . . 8
⊢ (𝑦 ∈ ({∅} ∖
{𝑥 ∈ {∅} ∣
𝜑}) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
41 | 40 | exlimiv 1591 |
. . . . . . 7
⊢
(∃𝑦 𝑦 ∈ ({∅} ∖
{𝑥 ∈ {∅} ∣
𝜑}) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
42 | 35, 41 | syl 14 |
. . . . . 6
⊢
((({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 ∧ ∅ ∈ 𝑛) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
43 | 31, 42 | jaodan 792 |
. . . . 5
⊢
((({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 ∧ (𝑛 = ∅ ∨ ∅ ∈ 𝑛)) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
44 | 18, 43 | sylan2 284 |
. . . 4
⊢
((({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 ∧ 𝑛 ∈ ω) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
45 | 44 | ancoms 266 |
. . 3
⊢ ((𝑛 ∈ ω ∧ ({∅}
∖ {𝑥 ∈ {∅}
∣ 𝜑}) ≈ 𝑛) → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
46 | 45 | rexlimiva 2582 |
. 2
⊢
(∃𝑛 ∈
ω ({∅} ∖ {𝑥 ∈ {∅} ∣ 𝜑}) ≈ 𝑛 → (¬ 𝜑 ∨ ¬ ¬ 𝜑)) |
47 | 17, 46 | ax-mp 5 |
1
⊢ (¬
𝜑 ∨ ¬ ¬ 𝜑) |