Step | Hyp | Ref
| Expression |
1 | | eldifn 3766 |
. . . . . 6
⊢ (𝑦 ∈ (ω ∖ 𝐴) → ¬ 𝑦 ∈ 𝐴) |
2 | 1 | adantl 481 |
. . . . 5
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ 𝑦 ∈ 𝐴) |
3 | | eldifi 3765 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ω ∖ 𝐴) → 𝑦 ∈ ω) |
4 | 3 | adantl 481 |
. . . . . . . . 9
⊢ ((∅
∈ 𝐴 ∧ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦 ∈ ω) |
5 | | elndif 3767 |
. . . . . . . . . 10
⊢ (∅
∈ 𝐴 → ¬
∅ ∈ (ω ∖ 𝐴)) |
6 | | eleq1 2718 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (𝑦 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω
∖ 𝐴))) |
7 | 6 | biimpcd 239 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ω ∖ 𝐴) → (𝑦 = ∅ → ∅ ∈ (ω
∖ 𝐴))) |
8 | 7 | necon3bd 2837 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈
(ω ∖ 𝐴) →
𝑦 ≠
∅)) |
9 | 5, 8 | mpan9 485 |
. . . . . . . . 9
⊢ ((∅
∈ 𝐴 ∧ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦 ≠ ∅) |
10 | | nnsuc 7124 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝑦 ≠ ∅) →
∃𝑥 ∈ ω
𝑦 = suc 𝑥) |
11 | 4, 9, 10 | syl2anc 694 |
. . . . . . . 8
⊢ ((∅
∈ 𝐴 ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
12 | 11 | adantlr 751 |
. . . . . . 7
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
13 | 12 | adantr 480 |
. . . . . 6
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
14 | | nfra1 2970 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) |
15 | | nfv 1883 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
16 | 14, 15 | nfan 1868 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) |
17 | | nfv 1883 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
18 | | rsp 2958 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) |
19 | | vex 3234 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
20 | 19 | sucid 5842 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ suc 𝑥 |
21 | | eleq2 2719 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = suc 𝑥 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ suc 𝑥)) |
22 | 20, 21 | mpbiri 248 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = suc 𝑥 → 𝑥 ∈ 𝑦) |
23 | | eleq1 2718 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ suc 𝑥 ∈ ω)) |
24 | | peano2b 7123 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈
ω) |
25 | 23, 24 | syl6bbr 278 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ 𝑥 ∈ ω)) |
26 | | minel 4066 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ¬ 𝑥 ∈ (ω ∖ 𝐴)) |
27 | | neldif 3768 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ω ∧ ¬
𝑥 ∈ (ω ∖
𝐴)) → 𝑥 ∈ 𝐴) |
28 | 26, 27 | sylan2 490 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ω ∧ (𝑥 ∈ 𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐴) |
29 | 28 | exp32 630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ω → (𝑥 ∈ 𝑦 → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥 ∈ 𝐴))) |
30 | 25, 29 | syl6bi 243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = suc 𝑥 → (𝑦 ∈ ω → (𝑥 ∈ 𝑦 → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥 ∈ 𝐴)))) |
31 | 22, 30 | mpid 44 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = suc 𝑥 → (𝑦 ∈ ω → (((ω ∖
𝐴) ∩ 𝑦) = ∅ → 𝑥 ∈ 𝐴))) |
32 | 3, 31 | syl5 34 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = suc 𝑥 → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → 𝑥 ∈ 𝐴))) |
33 | 32 | impd 446 |
. . . . . . . . . . . . 13
⊢ (𝑦 = suc 𝑥 → ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑥 ∈ 𝐴)) |
34 | | eleq1a 2725 |
. . . . . . . . . . . . . 14
⊢ (suc
𝑥 ∈ 𝐴 → (𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴)) |
35 | 34 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝑦 = suc 𝑥 → (suc 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
36 | 33, 35 | imim12d 81 |
. . . . . . . . . . . 12
⊢ (𝑦 = suc 𝑥 → ((𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑦 ∈ 𝐴))) |
37 | 36 | com13 88 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ((𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴))) |
38 | 18, 37 | sylan9 690 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → (𝑥 ∈ ω → (𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴))) |
39 | 16, 17, 38 | rexlimd 3055 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴)) |
40 | 39 | exp32 630 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴)))) |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (∅
∈ 𝐴 →
(∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴))))) |
42 | 41 | imp41 618 |
. . . . . 6
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴)) |
43 | 13, 42 | mpd 15 |
. . . . 5
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑦 ∈ 𝐴) |
44 | 2, 43 | mtand 692 |
. . . 4
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
45 | 44 | nrexdv 3030 |
. . 3
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ¬ ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
46 | | ordom 7116 |
. . . . 5
⊢ Ord
ω |
47 | | difss 3770 |
. . . . 5
⊢ (ω
∖ 𝐴) ⊆
ω |
48 | | tz7.5 5782 |
. . . . 5
⊢ ((Ord
ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖
𝐴) ≠ ∅) →
∃𝑦 ∈ (ω
∖ 𝐴)((ω ∖
𝐴) ∩ 𝑦) = ∅) |
49 | 46, 47, 48 | mp3an12 1454 |
. . . 4
⊢ ((ω
∖ 𝐴) ≠ ∅
→ ∃𝑦 ∈
(ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
50 | 49 | necon1bi 2851 |
. . 3
⊢ (¬
∃𝑦 ∈ (ω
∖ 𝐴)((ω ∖
𝐴) ∩ 𝑦) = ∅ → (ω ∖ 𝐴) = ∅) |
51 | 45, 50 | syl 17 |
. 2
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → (ω ∖ 𝐴) = ∅) |
52 | | ssdif0 3975 |
. 2
⊢ (ω
⊆ 𝐴 ↔ (ω
∖ 𝐴) =
∅) |
53 | 51, 52 | sylibr 224 |
1
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) |