| Step | Hyp | Ref
| Expression |
| 1 | | peano1 7910 |
. . . . . 6
⊢ ∅
∈ ω |
| 2 | | ne0i 4341 |
. . . . . 6
⊢ (∅
∈ ω → ω ≠ ∅) |
| 3 | | brwdomn0 9609 |
. . . . . 6
⊢ (ω
≠ ∅ → (ω ≼* 𝐴 ↔ ∃𝑓 𝑓:𝐴–onto→ω)) |
| 4 | 1, 2, 3 | mp2b 10 |
. . . . 5
⊢ (ω
≼* 𝐴
↔ ∃𝑓 𝑓:𝐴–onto→ω) |
| 5 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
| 6 | | fof 6820 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → 𝑓:𝐴⟶ω) |
| 7 | | dmfex 7927 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐴⟶ω) → 𝐴 ∈ V) |
| 8 | 5, 6, 7 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → 𝐴 ∈ V) |
| 9 | | cnvimass 6100 |
. . . . . . . . . 10
⊢ (◡𝑓 “ ran 𝐸) ⊆ dom 𝑓 |
| 10 | 9, 6 | fssdm 6755 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ran 𝐸) ⊆ 𝐴) |
| 11 | 8, 10 | sselpwd 5328 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴) |
| 12 | | fin1a2lem.b |
. . . . . . . . . . . . . 14
⊢ 𝐸 = (𝑥 ∈ ω ↦ (2o
·o 𝑥)) |
| 13 | 12 | fin1a2lem4 10443 |
. . . . . . . . . . . . 13
⊢ 𝐸:ω–1-1→ω |
| 14 | | f1cnv 6872 |
. . . . . . . . . . . . 13
⊢ (𝐸:ω–1-1→ω → ◡𝐸:ran 𝐸–1-1-onto→ω) |
| 15 | | f1ofo 6855 |
. . . . . . . . . . . . 13
⊢ (◡𝐸:ran 𝐸–1-1-onto→ω → ◡𝐸:ran 𝐸–onto→ω) |
| 16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ◡𝐸:ran 𝐸–onto→ω |
| 17 | | fofun 6821 |
. . . . . . . . . . . 12
⊢ (◡𝐸:ran 𝐸–onto→ω → Fun ◡𝐸) |
| 18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun ◡𝐸 |
| 19 | 5 | resex 6047 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (◡𝑓 “ ran 𝐸)) ∈ V |
| 20 | | cofunexg 7973 |
. . . . . . . . . . 11
⊢ ((Fun
◡𝐸 ∧ (𝑓 ↾ (◡𝑓 “ ran 𝐸)) ∈ V) → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V) |
| 21 | 18, 19, 20 | mp2an 692 |
. . . . . . . . . 10
⊢ (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V |
| 22 | | fofun 6821 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → Fun 𝑓) |
| 23 | | fores 6830 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (◡𝑓 “ ran 𝐸) ⊆ dom 𝑓) → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸))) |
| 24 | 22, 9, 23 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸))) |
| 25 | | f1f 6804 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:ω–1-1→ω → 𝐸:ω⟶ω) |
| 26 | | frn 6743 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:ω⟶ω →
ran 𝐸 ⊆
ω) |
| 27 | 13, 25, 26 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ran 𝐸 ⊆
ω |
| 28 | | foimacnv 6865 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–onto→ω ∧ ran 𝐸 ⊆ ω) → (𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸) |
| 29 | 27, 28 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸) |
| 30 | | foeq3 6818 |
. . . . . . . . . . . . 13
⊢ ((𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸 → ((𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸)) |
| 31 | 29, 30 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → ((𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸)) |
| 32 | 24, 31 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸) |
| 33 | | foco 6834 |
. . . . . . . . . . 11
⊢ ((◡𝐸:ran 𝐸–onto→ω ∧ (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸) → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) |
| 34 | 16, 32, 33 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) |
| 35 | | fowdom 9611 |
. . . . . . . . . 10
⊢ (((◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V ∧ (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) → ω ≼*
(◡𝑓 “ ran 𝐸)) |
| 36 | 21, 34, 35 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → ω ≼*
(◡𝑓 “ ran 𝐸)) |
| 37 | 5 | cnvex 7947 |
. . . . . . . . . . . 12
⊢ ◡𝑓 ∈ V |
| 38 | 37 | imaex 7936 |
. . . . . . . . . . 11
⊢ (◡𝑓 “ ran 𝐸) ∈ V |
| 39 | | isfin3-2 10407 |
. . . . . . . . . . 11
⊢ ((◡𝑓 “ ran 𝐸) ∈ V → ((◡𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬
ω ≼* (◡𝑓 “ ran 𝐸))) |
| 40 | 38, 39 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((◡𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬
ω ≼* (◡𝑓 “ ran 𝐸)) |
| 41 | 40 | con2bii 357 |
. . . . . . . . 9
⊢ (ω
≼* (◡𝑓 “ ran 𝐸) ↔ ¬ (◡𝑓 “ ran 𝐸) ∈ FinIII) |
| 42 | 36, 41 | sylib 218 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → ¬ (◡𝑓 “ ran 𝐸) ∈ FinIII) |
| 43 | | fin1a2lem.aa |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥) |
| 44 | 12, 43 | fin1a2lem6 10445 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ↾ ran 𝐸):ran 𝐸–1-1-onto→(ω ∖ ran 𝐸) |
| 45 | | f1ocnv 6860 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ↾ ran 𝐸):ran 𝐸–1-1-onto→(ω ∖ ran 𝐸) → ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran
𝐸) |
| 46 | | f1ofo 6855 |
. . . . . . . . . . . . . 14
⊢ (◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran
𝐸 → ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) |
| 47 | 44, 45, 46 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸 |
| 48 | | foco 6834 |
. . . . . . . . . . . . 13
⊢ ((◡𝐸:ran 𝐸–onto→ω ∧ ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) → (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω) |
| 49 | 16, 47, 48 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω |
| 50 | | fofun 6821 |
. . . . . . . . . . . 12
⊢ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω → Fun (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸))) |
| 51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun
(◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) |
| 52 | 5 | resex 6047 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ∈ V |
| 53 | | cofunexg 7973 |
. . . . . . . . . . 11
⊢ ((Fun
(◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∧ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ∈ V) → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V) |
| 54 | 51, 52, 53 | mp2an 692 |
. . . . . . . . . 10
⊢ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V |
| 55 | | difss 4136 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ 𝐴 |
| 56 | 6 | fdmd 6746 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → dom 𝑓 = 𝐴) |
| 57 | 55, 56 | sseqtrrid 4027 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓) |
| 58 | | fores 6830 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓) → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
| 59 | 22, 57, 58 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
| 60 | | funcnvcnv 6633 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑓 → Fun ◡◡𝑓) |
| 61 | | imadif 6650 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡◡𝑓 → (◡𝑓 “ (ω ∖ ran 𝐸)) = ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) |
| 62 | 22, 60, 61 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ (ω ∖ ran 𝐸)) = ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) |
| 63 | 62 | imaeq2d 6078 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (𝑓 “ ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸)))) |
| 64 | | difss 4136 |
. . . . . . . . . . . . . . 15
⊢ (ω
∖ ran 𝐸) ⊆
ω |
| 65 | | foimacnv 6865 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–onto→ω ∧ (ω ∖ ran 𝐸) ⊆ ω) → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸)) |
| 66 | 64, 65 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸)) |
| 67 | | fimacnv 6758 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴⟶ω → (◡𝑓 “ ω) = 𝐴) |
| 68 | 6, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ω) = 𝐴) |
| 69 | 68 | difeq1d 4125 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–onto→ω → ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸)) = (𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
| 70 | 69 | imaeq2d 6078 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) = (𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
| 71 | 63, 66, 70 | 3eqtr3rd 2786 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸)) |
| 72 | | foeq3 6818 |
. . . . . . . . . . . . 13
⊢ ((𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸) → ((𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸))) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → ((𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸))) |
| 74 | 59, 73 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) |
| 75 | | foco 6834 |
. . . . . . . . . . 11
⊢ (((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω ∧ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) |
| 76 | 49, 74, 75 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) |
| 77 | | fowdom 9611 |
. . . . . . . . . 10
⊢ ((((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V ∧ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) → ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
| 78 | 54, 76, 77 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
| 79 | | difexg 5329 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ V) |
| 80 | | isfin3-2 10407 |
. . . . . . . . . . 11
⊢ ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ V → ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬
ω ≼* (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
| 81 | 8, 79, 80 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬
ω ≼* (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
| 82 | 81 | con2bid 354 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → (ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ↔ ¬ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
| 83 | 78, 82 | mpbid 232 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → ¬ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII) |
| 84 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (𝑦 ∈ FinIII ↔ (◡𝑓 “ ran 𝐸) ∈
FinIII)) |
| 85 | | difeq2 4120 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (𝐴 ∖ 𝑦) = (𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
| 86 | 85 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → ((𝐴 ∖ 𝑦) ∈ FinIII ↔ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
| 87 | 84, 86 | orbi12d 919 |
. . . . . . . . . . 11
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → ((𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ ((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
| 88 | 87 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ ¬
((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
| 89 | | ioran 986 |
. . . . . . . . . 10
⊢ (¬
((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII) ↔ (¬
(◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
| 90 | 88, 89 | bitrdi 287 |
. . . . . . . . 9
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ (¬
(◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
| 91 | 90 | rspcev 3622 |
. . . . . . . 8
⊢ (((◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴 ∧ (¬ (◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII)) →
∃𝑦 ∈ 𝒫
𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
| 92 | 11, 42, 83, 91 | syl12anc 837 |
. . . . . . 7
⊢ (𝑓:𝐴–onto→ω → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
| 93 | | rexnal 3100 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈ FinIII)
↔ ¬ ∀𝑦
∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈
FinIII)) |
| 94 | 92, 93 | sylib 218 |
. . . . . 6
⊢ (𝑓:𝐴–onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
| 95 | 94 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑓 𝑓:𝐴–onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
| 96 | 4, 95 | sylbi 217 |
. . . 4
⊢ (ω
≼* 𝐴
→ ¬ ∀𝑦
∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈
FinIII)) |
| 97 | 96 | con2i 139 |
. . 3
⊢
(∀𝑦 ∈
𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈ FinIII)
→ ¬ ω ≼* 𝐴) |
| 98 | | isfin3-2 10407 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ¬
ω ≼* 𝐴)) |
| 99 | 97, 98 | imbitrrid 246 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) → 𝐴 ∈
FinIII)) |
| 100 | 99 | imp 406 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) → 𝐴 ∈
FinIII) |