Step | Hyp | Ref
| Expression |
1 | | peano1 7667 |
. . . . . 6
⊢ ∅
∈ ω |
2 | | ne0i 4249 |
. . . . . 6
⊢ (∅
∈ ω → ω ≠ ∅) |
3 | | brwdomn0 9185 |
. . . . . 6
⊢ (ω
≠ ∅ → (ω ≼* 𝐴 ↔ ∃𝑓 𝑓:𝐴–onto→ω)) |
4 | 1, 2, 3 | mp2b 10 |
. . . . 5
⊢ (ω
≼* 𝐴
↔ ∃𝑓 𝑓:𝐴–onto→ω) |
5 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
6 | | fof 6633 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → 𝑓:𝐴⟶ω) |
7 | | dmfex 7685 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐴⟶ω) → 𝐴 ∈ V) |
8 | 5, 6, 7 | sylancr 590 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → 𝐴 ∈ V) |
9 | | cnvimass 5949 |
. . . . . . . . . 10
⊢ (◡𝑓 “ ran 𝐸) ⊆ dom 𝑓 |
10 | 9, 6 | fssdm 6565 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ran 𝐸) ⊆ 𝐴) |
11 | 8, 10 | sselpwd 5219 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴) |
12 | | fin1a2lem.b |
. . . . . . . . . . . . . 14
⊢ 𝐸 = (𝑥 ∈ ω ↦ (2o
·o 𝑥)) |
13 | 12 | fin1a2lem4 10017 |
. . . . . . . . . . . . 13
⊢ 𝐸:ω–1-1→ω |
14 | | f1cnv 6684 |
. . . . . . . . . . . . 13
⊢ (𝐸:ω–1-1→ω → ◡𝐸:ran 𝐸–1-1-onto→ω) |
15 | | f1ofo 6668 |
. . . . . . . . . . . . 13
⊢ (◡𝐸:ran 𝐸–1-1-onto→ω → ◡𝐸:ran 𝐸–onto→ω) |
16 | 13, 14, 15 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ◡𝐸:ran 𝐸–onto→ω |
17 | | fofun 6634 |
. . . . . . . . . . . 12
⊢ (◡𝐸:ran 𝐸–onto→ω → Fun ◡𝐸) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun ◡𝐸 |
19 | 5 | resex 5899 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (◡𝑓 “ ran 𝐸)) ∈ V |
20 | | cofunexg 7722 |
. . . . . . . . . . 11
⊢ ((Fun
◡𝐸 ∧ (𝑓 ↾ (◡𝑓 “ ran 𝐸)) ∈ V) → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V) |
21 | 18, 19, 20 | mp2an 692 |
. . . . . . . . . 10
⊢ (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V |
22 | | fofun 6634 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → Fun 𝑓) |
23 | | fores 6643 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (◡𝑓 “ ran 𝐸) ⊆ dom 𝑓) → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸))) |
24 | 22, 9, 23 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸))) |
25 | | f1f 6615 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:ω–1-1→ω → 𝐸:ω⟶ω) |
26 | | frn 6552 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:ω⟶ω →
ran 𝐸 ⊆
ω) |
27 | 13, 25, 26 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ran 𝐸 ⊆
ω |
28 | | foimacnv 6678 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–onto→ω ∧ ran 𝐸 ⊆ ω) → (𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸) |
29 | 27, 28 | mpan2 691 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸) |
30 | | foeq3 6631 |
. . . . . . . . . . . . 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 235 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸) |
33 | | foco 6647 |
. . . . . . . . . . 11
⊢ ((◡𝐸:ran 𝐸–onto→ω ∧ (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸) → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) |
34 | 16, 32, 33 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) |
35 | | fowdom 9187 |
. . . . . . . . . 10
⊢ (((◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V ∧ (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) → ω ≼*
(◡𝑓 “ ran 𝐸)) |
36 | 21, 34, 35 | sylancr 590 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → ω ≼*
(◡𝑓 “ ran 𝐸)) |
37 | 5 | cnvex 7703 |
. . . . . . . . . . . 12
⊢ ◡𝑓 ∈ V |
38 | 37 | imaex 7694 |
. . . . . . . . . . 11
⊢ (◡𝑓 “ ran 𝐸) ∈ V |
39 | | isfin3-2 9981 |
. . . . . . . . . . 11
⊢ ((◡𝑓 “ ran 𝐸) ∈ V → ((◡𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬
ω ≼* (◡𝑓 “ ran 𝐸))) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((◡𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬
ω ≼* (◡𝑓 “ ran 𝐸)) |
41 | 40 | con2bii 361 |
. . . . . . . . 9
⊢ (ω
≼* (◡𝑓 “ ran 𝐸) ↔ ¬ (◡𝑓 “ ran 𝐸) ∈ FinIII) |
42 | 36, 41 | sylib 221 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → ¬ (◡𝑓 “ ran 𝐸) ∈ FinIII) |
43 | | fin1a2lem.aa |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥) |
44 | 12, 43 | fin1a2lem6 10019 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ↾ ran 𝐸):ran 𝐸–1-1-onto→(ω ∖ ran 𝐸) |
45 | | f1ocnv 6673 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ↾ ran 𝐸):ran 𝐸–1-1-onto→(ω ∖ ran 𝐸) → ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran
𝐸) |
46 | | f1ofo 6668 |
. . . . . . . . . . . . . 14
⊢ (◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran
𝐸 → ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) |
47 | 44, 45, 46 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸 |
48 | | foco 6647 |
. . . . . . . . . . . . 13
⊢ ((◡𝐸:ran 𝐸–onto→ω ∧ ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) → (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω) |
49 | 16, 47, 48 | mp2an 692 |
. . . . . . . . . . . 12
⊢ (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω |
50 | | fofun 6634 |
. . . . . . . . . . . 12
⊢ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω → Fun (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸))) |
51 | 49, 50 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun
(◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) |
52 | 5 | resex 5899 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ∈ V |
53 | | cofunexg 7722 |
. . . . . . . . . . 11
⊢ ((Fun
(◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∧ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ∈ V) → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V) |
54 | 51, 52, 53 | mp2an 692 |
. . . . . . . . . 10
⊢ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V |
55 | | difss 4046 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ 𝐴 |
56 | 6 | fdmd 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → dom 𝑓 = 𝐴) |
57 | 55, 56 | sseqtrrid 3954 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓) |
58 | | fores 6643 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓) → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
59 | 22, 57, 58 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
60 | | funcnvcnv 6447 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑓 → Fun ◡◡𝑓) |
61 | | imadif 6464 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡◡𝑓 → (◡𝑓 “ (ω ∖ ran 𝐸)) = ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) |
62 | 22, 60, 61 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ (ω ∖ ran 𝐸)) = ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) |
63 | 62 | imaeq2d 5929 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (𝑓 “ ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸)))) |
64 | | difss 4046 |
. . . . . . . . . . . . . . 15
⊢ (ω
∖ ran 𝐸) ⊆
ω |
65 | | foimacnv 6678 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–onto→ω ∧ (ω ∖ ran 𝐸) ⊆ ω) → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸)) |
66 | 64, 65 | mpan2 691 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸)) |
67 | | fimacnv 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴⟶ω → (◡𝑓 “ ω) = 𝐴) |
68 | 6, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ω) = 𝐴) |
69 | 68 | difeq1d 4036 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–onto→ω → ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸)) = (𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
70 | 69 | imaeq2d 5929 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) = (𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
71 | 63, 66, 70 | 3eqtr3rd 2786 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸)) |
72 | | foeq3 6631 |
. . . . . . . . . . . . 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 235 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) |
75 | | foco 6647 |
. . . . . . . . . . 11
⊢ (((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω ∧ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) |
76 | 49, 74, 75 | sylancr 590 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) |
77 | | fowdom 9187 |
. . . . . . . . . 10
⊢ ((((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V ∧ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) → ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
78 | 54, 76, 77 | sylancr 590 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
79 | | difexg 5220 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ V) |
80 | | isfin3-2 9981 |
. . . . . . . . . . 11
⊢ ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ V → ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬
ω ≼* (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
81 | 8, 79, 80 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬
ω ≼* (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
82 | 81 | con2bid 358 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → (ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ↔ ¬ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
83 | 78, 82 | mpbid 235 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → ¬ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII) |
84 | | eleq1 2825 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (𝑦 ∈ FinIII ↔ (◡𝑓 “ ran 𝐸) ∈
FinIII)) |
85 | | difeq2 4031 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (𝐴 ∖ 𝑦) = (𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
86 | 85 | eleq1d 2822 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → ((𝐴 ∖ 𝑦) ∈ FinIII ↔ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
87 | 84, 86 | orbi12d 919 |
. . . . . . . . . . 11
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → ((𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ ((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
88 | 87 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ ¬
((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
89 | | ioran 984 |
. . . . . . . . . 10
⊢ (¬
((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII) ↔ (¬
(◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
90 | 88, 89 | bitrdi 290 |
. . . . . . . . 9
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ (¬
(◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
91 | 90 | rspcev 3537 |
. . . . . . . 8
⊢ (((◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴 ∧ (¬ (◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII)) →
∃𝑦 ∈ 𝒫
𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
92 | 11, 42, 83, 91 | syl12anc 837 |
. . . . . . 7
⊢ (𝑓:𝐴–onto→ω → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
93 | | rexnal 3160 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈ FinIII)
↔ ¬ ∀𝑦
∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈
FinIII)) |
94 | 92, 93 | sylib 221 |
. . . . . 6
⊢ (𝑓:𝐴–onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
95 | 94 | exlimiv 1938 |
. . . . 5
⊢
(∃𝑓 𝑓:𝐴–onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
96 | 4, 95 | sylbi 220 |
. . . 4
⊢ (ω
≼* 𝐴
→ ¬ ∀𝑦
∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈
FinIII)) |
97 | 96 | con2i 141 |
. . 3
⊢
(∀𝑦 ∈
𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈ FinIII)
→ ¬ ω ≼* 𝐴) |
98 | | isfin3-2 9981 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ¬
ω ≼* 𝐴)) |
99 | 97, 98 | syl5ibr 249 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) → 𝐴 ∈
FinIII)) |
100 | 99 | imp 410 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) → 𝐴 ∈
FinIII) |