| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eldifn 4132 | . . . . . 6
⊢ (𝑧 ∈ (ω ∖ 𝐴) → ¬ 𝑧 ∈ 𝐴) | 
| 2 | 1 | adantl 481 | . . . . 5
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ 𝑧 ∈ 𝐴) | 
| 3 |  | eldifi 4131 | . . . . . . . 8
⊢ (𝑧 ∈ (ω ∖ 𝐴) → 𝑧 ∈ ω) | 
| 4 |  | elndif 4133 | . . . . . . . . 9
⊢ (∅
∈ 𝐴 → ¬
∅ ∈ (ω ∖ 𝐴)) | 
| 5 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑧 ∈ (ω ∖ 𝐴) ↔ ∅ ∈ (ω
∖ 𝐴))) | 
| 6 | 5 | biimpcd 249 | . . . . . . . . . 10
⊢ (𝑧 ∈ (ω ∖ 𝐴) → (𝑧 = ∅ → ∅ ∈ (ω
∖ 𝐴))) | 
| 7 | 6 | necon3bd 2954 | . . . . . . . . 9
⊢ (𝑧 ∈ (ω ∖ 𝐴) → (¬ ∅ ∈
(ω ∖ 𝐴) →
𝑧 ≠
∅)) | 
| 8 | 4, 7 | mpan9 506 | . . . . . . . 8
⊢ ((∅
∈ 𝐴 ∧ 𝑧 ∈ (ω ∖ 𝐴)) → 𝑧 ≠ ∅) | 
| 9 |  | nnsuc 7905 | . . . . . . . 8
⊢ ((𝑧 ∈ ω ∧ 𝑧 ≠ ∅) →
∃𝑦 ∈ ω
𝑧 = suc 𝑦) | 
| 10 | 3, 8, 9 | syl2an2 686 | . . . . . . 7
⊢ ((∅
∈ 𝐴 ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦) | 
| 11 | 10 | ad4ant13 751 | . . . . . 6
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ∃𝑦 ∈ ω 𝑧 = suc 𝑦) | 
| 12 |  | eleq1w 2824 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | 
| 13 |  | suceq 6450 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦) | 
| 14 | 13 | eleq1d 2826 | . . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (suc 𝑥 ∈ 𝐴 ↔ suc 𝑦 ∈ 𝐴)) | 
| 15 | 12, 14 | imbi12d 344 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ↔ (𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴))) | 
| 16 | 15 | rspccv 3619 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑦 ∈ ω → (𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴))) | 
| 17 |  | vex 3484 | . . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V | 
| 18 | 17 | sucid 6466 | . . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ suc 𝑦 | 
| 19 |  | eleq2 2830 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = suc 𝑦 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ suc 𝑦)) | 
| 20 | 18, 19 | mpbiri 258 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = suc 𝑦 → 𝑦 ∈ 𝑧) | 
| 21 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ suc 𝑦 ∈ ω)) | 
| 22 |  | peano2b 7904 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈
ω) | 
| 23 | 21, 22 | bitr4di 289 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = suc 𝑦 → (𝑧 ∈ ω ↔ 𝑦 ∈ ω)) | 
| 24 |  | minel 4466 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ 𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ¬ 𝑦 ∈ (ω ∖ 𝐴)) | 
| 25 |  | neldif 4134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ω ∧ ¬
𝑦 ∈ (ω ∖
𝐴)) → 𝑦 ∈ 𝐴) | 
| 26 | 24, 25 | sylan2 593 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ω ∧ (𝑦 ∈ 𝑧 ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → 𝑦 ∈ 𝐴) | 
| 27 | 26 | exp32 420 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ω → (𝑦 ∈ 𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦 ∈ 𝐴))) | 
| 28 | 23, 27 | biimtrdi 253 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (𝑦 ∈ 𝑧 → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦 ∈ 𝐴)))) | 
| 29 | 20, 28 | mpid 44 | . . . . . . . . . . . . . . 15
⊢ (𝑧 = suc 𝑦 → (𝑧 ∈ ω → (((ω ∖
𝐴) ∩ 𝑧) = ∅ → 𝑦 ∈ 𝐴))) | 
| 30 | 3, 29 | syl5 34 | . . . . . . . . . . . . . 14
⊢ (𝑧 = suc 𝑦 → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → 𝑦 ∈ 𝐴))) | 
| 31 | 30 | impd 410 | . . . . . . . . . . . . 13
⊢ (𝑧 = suc 𝑦 → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑦 ∈ 𝐴)) | 
| 32 |  | eleq1a 2836 | . . . . . . . . . . . . . 14
⊢ (suc
𝑦 ∈ 𝐴 → (𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴)) | 
| 33 | 32 | com12 32 | . . . . . . . . . . . . 13
⊢ (𝑧 = suc 𝑦 → (suc 𝑦 ∈ 𝐴 → 𝑧 ∈ 𝐴)) | 
| 34 | 31, 33 | imim12d 81 | . . . . . . . . . . . 12
⊢ (𝑧 = suc 𝑦 → ((𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴) → ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧 ∈ 𝐴))) | 
| 35 | 34 | com13 88 | . . . . . . . . . . 11
⊢ ((𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → ((𝑦 ∈ 𝐴 → suc 𝑦 ∈ 𝐴) → (𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴))) | 
| 36 | 16, 35 | sylan9 507 | . . . . . . . . . 10
⊢
((∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (𝑦 ∈ ω → (𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴))) | 
| 37 | 36 | rexlimdv 3153 | . . . . . . . . 9
⊢
((∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ (ω ∖ 𝐴) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅)) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴)) | 
| 38 | 37 | exp32 420 | . . . . . . . 8
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴)))) | 
| 39 | 38 | a1i 11 | . . . . . . 7
⊢ (∅
∈ 𝐴 →
(∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → (𝑧 ∈ (ω ∖ 𝐴) → (((ω ∖ 𝐴) ∩ 𝑧) = ∅ → (∃𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴))))) | 
| 40 | 39 | imp41 425 | . . . . . 6
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → (∃𝑦 ∈ ω 𝑧 = suc 𝑦 → 𝑧 ∈ 𝐴)) | 
| 41 | 11, 40 | mpd 15 | . . . . 5
⊢
((((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) ∧ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) → 𝑧 ∈ 𝐴) | 
| 42 | 2, 41 | mtand 816 | . . . 4
⊢
(((∅ ∈ 𝐴
∧ ∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) ∧ 𝑧 ∈ (ω ∖ 𝐴)) → ¬ ((ω ∖ 𝐴) ∩ 𝑧) = ∅) | 
| 43 | 42 | nrexdv 3149 | . . 3
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ¬ ∃𝑧 ∈ (ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅) | 
| 44 |  | ordom 7897 | . . . . 5
⊢ Ord
ω | 
| 45 |  | difss 4136 | . . . . 5
⊢ (ω
∖ 𝐴) ⊆
ω | 
| 46 |  | tz7.5 6405 | . . . . 5
⊢ ((Ord
ω ∧ (ω ∖ 𝐴) ⊆ ω ∧ (ω ∖
𝐴) ≠ ∅) →
∃𝑧 ∈ (ω
∖ 𝐴)((ω ∖
𝐴) ∩ 𝑧) = ∅) | 
| 47 | 44, 45, 46 | mp3an12 1453 | . . . 4
⊢ ((ω
∖ 𝐴) ≠ ∅
→ ∃𝑧 ∈
(ω ∖ 𝐴)((ω ∖ 𝐴) ∩ 𝑧) = ∅) | 
| 48 | 47 | necon1bi 2969 | . . 3
⊢ (¬
∃𝑧 ∈ (ω
∖ 𝐴)((ω ∖
𝐴) ∩ 𝑧) = ∅ → (ω ∖ 𝐴) = ∅) | 
| 49 | 43, 48 | syl 17 | . 2
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → (ω ∖ 𝐴) = ∅) | 
| 50 |  | ssdif0 4366 | . 2
⊢ (ω
⊆ 𝐴 ↔ (ω
∖ 𝐴) =
∅) | 
| 51 | 49, 50 | sylibr 234 | 1
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) |