Step | Hyp | Ref
| Expression |
1 | | eldifn 3733 |
. . . . . 6
⊢ (𝑦 ∈ (ω ∖ 𝐴) → ¬ 𝑦 ∈ 𝐴) |
2 | 1 | adantl 482 |
. . . . 5
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ 𝑦 ∈ 𝐴) |
3 | | eldifi 3732 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ω ∖ 𝐴) → 𝑦 ∈ ω) |
4 | 3 | adantl 482 |
. . . . . . . . 9
⊢ ((∅
∈ 𝐴 ∧ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦 ∈ ω) |
5 | | elndif 3734 |
. . . . . . . . . 10
⊢ (∅
∈ 𝐴 → ¬
∅ ∈ (ω ∖ 𝐴)) |
6 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∅ → (𝑦 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω
∖ 𝐴))) |
7 | 6 | biimpcd 239 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (ω ∖ 𝐴) → (𝑦 = ∅ → ∅ ∈ (ω
∖ 𝐴))) |
8 | 7 | necon3bd 2808 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈
(ω ∖ 𝐴) →
𝑦 ≠
∅)) |
9 | 5, 8 | mpan9 486 |
. . . . . . . . 9
⊢ ((∅
∈ 𝐴 ∧ 𝑦 ∈ (ω ∖ 𝐴)) → 𝑦 ≠ ∅) |
10 | | nnsuc 7082 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧ 𝑦 ≠ ∅) →
∃𝑥 ∈ ω
𝑦 = suc 𝑥) |
11 | 4, 9, 10 | syl2anc 693 |
. . . . . . . 8
⊢ ((∅
∈ 𝐴 ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
12 | 11 | adantlr 751 |
. . . . . . 7
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
13 | 12 | adantr 481 |
. . . . . 6
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥) |
14 | | nfra1 2941 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) |
15 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
16 | 14, 15 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) |
17 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ 𝐴 |
18 | | rsp 2929 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) |
19 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑥 ∈ V |
20 | 19 | sucid 5804 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ suc 𝑥 |
21 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = suc 𝑥 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ suc 𝑥)) |
22 | 20, 21 | mpbiri 248 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = suc 𝑥 → 𝑥 ∈ 𝑦) |
23 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ suc 𝑥 ∈ ω)) |
24 | | peano2b 7081 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ω ↔ suc 𝑥 ∈
ω) |
25 | 23, 24 | syl6bbr 278 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = suc 𝑥 → (𝑦 ∈ ω ↔ 𝑥 ∈ ω)) |
26 | | minel 4033 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → ¬ 𝑥 ∈ (ω ∖ 𝐴)) |
27 | | neldif 3735 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ω ∧ ¬
𝑥 ∈ (ω ∖
𝐴)) → 𝑥 ∈ 𝐴) |
28 | 26, 27 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ω ∧ (𝑥 ∈ 𝑦 ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → 𝑥 ∈ 𝐴) |
29 | 28 | exp32 631 |
. . . . . . . . . . . . . . . . 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 447 |
. . . . . . . . . . . . 13
⊢ (𝑦 = suc 𝑥 → ((𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑥 ∈ 𝐴)) |
34 | | eleq1a 2696 |
. . . . . . . . . . . . . 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 689 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → (𝑥 ∈ ω → (𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴))) |
39 | 16, 17, 38 | rexlimd 3026 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅)) → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴)) |
40 | 39 | exp32 631 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴)))) |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (∅
∈ 𝐴 →
(∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑦 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑦) = ∅ → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴))))) |
42 | 41 | imp41 619 |
. . . . . 6
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → (∃𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴)) |
43 | 13, 42 | mpd 15 |
. . . . 5
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) → 𝑦 ∈ 𝐴) |
44 | 2, 43 | mtand 691 |
. . . 4
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑦 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
45 | 44 | nrexdv 3001 |
. . 3
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ¬ ∃𝑦 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
46 | | ordom 7074 |
. . . . 5
⊢ Ord
ω |
47 | | difss 3737 |
. . . . 5
⊢ (ω
∖ 𝐴) ⊆
ω |
48 | | tz7.5 5744 |
. . . . 5
⊢ ((Ord
ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖
𝐴) ≠ ∅) →
∃𝑦 ∈ (ω
∖ 𝐴)((ω ∖
𝐴) ∩ 𝑦) = ∅) |
49 | 46, 47, 48 | mp3an12 1414 |
. . . 4
⊢ ((ω
∖ 𝐴) ≠ ∅
→ ∃𝑦 ∈
(ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑦) = ∅) |
50 | 49 | necon1bi 2822 |
. . 3
⊢ (¬
∃𝑦 ∈ (ω
∖ 𝐴)((ω ∖
𝐴) ∩ 𝑦) = ∅ → (ω ∖ 𝐴) = ∅) |
51 | 45, 50 | syl 17 |
. 2
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → (ω ∖ 𝐴) = ∅) |
52 | | ssdif0 3942 |
. 2
⊢ (ω
⊆ 𝐴 ↔ (ω
∖ 𝐴) =
∅) |
53 | 51, 52 | sylibr 224 |
1
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) |