Step | Hyp | Ref
| Expression |
1 | | peano1 6977 |
. . . . . 6
⊢ ∅
∈ ω |
2 | | ne0i 3880 |
. . . . . 6
⊢ (∅
∈ ω → ω ≠ ∅) |
3 | | brwdomn0 8357 |
. . . . . 6
⊢ (ω
≠ ∅ → (ω ≼* 𝐴 ↔ ∃𝑓 𝑓:𝐴–onto→ω)) |
4 | 1, 2, 3 | mp2b 10 |
. . . . 5
⊢ (ω
≼* 𝐴
↔ ∃𝑓 𝑓:𝐴–onto→ω) |
5 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
6 | | fof 6028 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → 𝑓:𝐴⟶ω) |
7 | | dmfex 7017 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐴⟶ω) → 𝐴 ∈ V) |
8 | 5, 6, 7 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → 𝐴 ∈ V) |
9 | | cnvimass 5404 |
. . . . . . . . . 10
⊢ (◡𝑓 “ ran 𝐸) ⊆ dom 𝑓 |
10 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴⟶ω → dom 𝑓 = 𝐴) |
11 | 6, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → dom 𝑓 = 𝐴) |
12 | 9, 11 | syl5sseq 3616 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ran 𝐸) ⊆ 𝐴) |
13 | 8, 12 | sselpwd 4734 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴) |
14 | | fin1a2lem.b |
. . . . . . . . . . . . . 14
⊢ 𝐸 = (𝑥 ∈ ω ↦
(2𝑜 ·𝑜 𝑥)) |
15 | 14 | fin1a2lem4 9108 |
. . . . . . . . . . . . 13
⊢ 𝐸:ω–1-1→ω |
16 | | f1cnv 6073 |
. . . . . . . . . . . . 13
⊢ (𝐸:ω–1-1→ω → ◡𝐸:ran 𝐸–1-1-onto→ω) |
17 | | f1ofo 6057 |
. . . . . . . . . . . . 13
⊢ (◡𝐸:ran 𝐸–1-1-onto→ω → ◡𝐸:ran 𝐸–onto→ω) |
18 | 15, 16, 17 | mp2b 10 |
. . . . . . . . . . . 12
⊢ ◡𝐸:ran 𝐸–onto→ω |
19 | | fofun 6029 |
. . . . . . . . . . . 12
⊢ (◡𝐸:ran 𝐸–onto→ω → Fun ◡𝐸) |
20 | 18, 19 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun ◡𝐸 |
21 | 5 | resex 5363 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (◡𝑓 “ ran 𝐸)) ∈ V |
22 | | cofunexg 7023 |
. . . . . . . . . . 11
⊢ ((Fun
◡𝐸 ∧ (𝑓 ↾ (◡𝑓 “ ran 𝐸)) ∈ V) → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V) |
23 | 20, 21, 22 | mp2an 704 |
. . . . . . . . . 10
⊢ (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V |
24 | | fofun 6029 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → Fun 𝑓) |
25 | | fores 6037 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (◡𝑓 “ ran 𝐸) ⊆ dom 𝑓) → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸))) |
26 | 24, 9, 25 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸))) |
27 | | f1f 6014 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:ω–1-1→ω → 𝐸:ω⟶ω) |
28 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢ (𝐸:ω⟶ω →
ran 𝐸 ⊆
ω) |
29 | 15, 27, 28 | mp2b 10 |
. . . . . . . . . . . . . 14
⊢ ran 𝐸 ⊆
ω |
30 | | foimacnv 6067 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–onto→ω ∧ ran 𝐸 ⊆ ω) → (𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸) |
31 | 29, 30 | mpan2 703 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸) |
32 | | foeq3 6026 |
. . . . . . . . . . . . 13
⊢ ((𝑓 “ (◡𝑓 “ ran 𝐸)) = ran 𝐸 → ((𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → ((𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→(𝑓 “ (◡𝑓 “ ran 𝐸)) ↔ (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸)) |
34 | 26, 33 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸) |
35 | | foco 6038 |
. . . . . . . . . . 11
⊢ ((◡𝐸:ran 𝐸–onto→ω ∧ (𝑓 ↾ (◡𝑓 “ ran 𝐸)):(◡𝑓 “ ran 𝐸)–onto→ran 𝐸) → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) |
36 | 18, 34, 35 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) |
37 | | fowdom 8359 |
. . . . . . . . . 10
⊢ (((◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))) ∈ V ∧ (◡𝐸 ∘ (𝑓 ↾ (◡𝑓 “ ran 𝐸))):(◡𝑓 “ ran 𝐸)–onto→ω) → ω ≼*
(◡𝑓 “ ran 𝐸)) |
38 | 23, 36, 37 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → ω ≼*
(◡𝑓 “ ran 𝐸)) |
39 | 5 | cnvex 7006 |
. . . . . . . . . . . 12
⊢ ◡𝑓 ∈ V |
40 | 39 | imaex 6996 |
. . . . . . . . . . 11
⊢ (◡𝑓 “ ran 𝐸) ∈ V |
41 | | isfin3-2 9072 |
. . . . . . . . . . 11
⊢ ((◡𝑓 “ ran 𝐸) ∈ V → ((◡𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬
ω ≼* (◡𝑓 “ ran 𝐸))) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((◡𝑓 “ ran 𝐸) ∈ FinIII ↔ ¬
ω ≼* (◡𝑓 “ ran 𝐸)) |
43 | 42 | con2bii 346 |
. . . . . . . . 9
⊢ (ω
≼* (◡𝑓 “ ran 𝐸) ↔ ¬ (◡𝑓 “ ran 𝐸) ∈ FinIII) |
44 | 38, 43 | sylib 207 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → ¬ (◡𝑓 “ ran 𝐸) ∈ FinIII) |
45 | | fin1a2lem.aa |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (𝑥 ∈ On ↦ suc 𝑥) |
46 | 14, 45 | fin1a2lem6 9110 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ↾ ran 𝐸):ran 𝐸–1-1-onto→(ω ∖ ran 𝐸) |
47 | | f1ocnv 6062 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ↾ ran 𝐸):ran 𝐸–1-1-onto→(ω ∖ ran 𝐸) → ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran
𝐸) |
48 | | f1ofo 6057 |
. . . . . . . . . . . . . 14
⊢ (◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–1-1-onto→ran
𝐸 → ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) |
49 | 46, 47, 48 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸 |
50 | | foco 6038 |
. . . . . . . . . . . . 13
⊢ ((◡𝐸:ran 𝐸–onto→ω ∧ ◡(𝑆 ↾ ran 𝐸):(ω ∖ ran 𝐸)–onto→ran 𝐸) → (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω) |
51 | 18, 49, 50 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω |
52 | | fofun 6029 |
. . . . . . . . . . . 12
⊢ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω → Fun (◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸))) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun
(◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) |
54 | 5 | resex 5363 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ∈ V |
55 | | cofunexg 7023 |
. . . . . . . . . . 11
⊢ ((Fun
(◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∧ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ∈ V) → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V) |
56 | 53, 54, 55 | mp2an 704 |
. . . . . . . . . 10
⊢ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V |
57 | | difss 3699 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ 𝐴 |
58 | 57, 11 | syl5sseqr 3617 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓) |
59 | | fores 6037 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ⊆ dom 𝑓) → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
60 | 24, 58, 59 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
61 | | funcnvcnv 5870 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝑓 → Fun ◡◡𝑓) |
62 | | imadif 5887 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡◡𝑓 → (◡𝑓 “ (ω ∖ ran 𝐸)) = ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) |
63 | 24, 61, 62 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ (ω ∖ ran 𝐸)) = ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) |
64 | 63 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (𝑓 “ ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸)))) |
65 | | difss 3699 |
. . . . . . . . . . . . . . 15
⊢ (ω
∖ ran 𝐸) ⊆
ω |
66 | | foimacnv 6067 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–onto→ω ∧ (ω ∖ ran 𝐸) ⊆ ω) → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸)) |
67 | 65, 66 | mpan2 703 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (◡𝑓 “ (ω ∖ ran 𝐸))) = (ω ∖ ran 𝐸)) |
68 | | fimacnv 6255 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:𝐴⟶ω → (◡𝑓 “ ω) = 𝐴) |
69 | 6, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐴–onto→ω → (◡𝑓 “ ω) = 𝐴) |
70 | 69 | difeq1d 3689 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴–onto→ω → ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸)) = (𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
71 | 70 | imaeq2d 5385 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ ((◡𝑓 “ ω) ∖ (◡𝑓 “ ran 𝐸))) = (𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
72 | 64, 67, 71 | 3eqtr3rd 2653 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐴–onto→ω → (𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸)) |
73 | | foeq3 6026 |
. . . . . . . . . . . . 13
⊢ ((𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) = (ω ∖ ran 𝐸) → ((𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸))) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐴–onto→ω → ((𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(𝑓 “ (𝐴 ∖ (◡𝑓 “ ran 𝐸))) ↔ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸))) |
75 | 60, 74 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑓:𝐴–onto→ω → (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) |
76 | | foco 6038 |
. . . . . . . . . . 11
⊢ (((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)):(ω ∖ ran 𝐸)–onto→ω ∧ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→(ω ∖ ran 𝐸)) → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) |
77 | 51, 75, 76 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) |
78 | | fowdom 8359 |
. . . . . . . . . 10
⊢ ((((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) ∈ V ∧ ((◡𝐸 ∘ ◡(𝑆 ↾ ran 𝐸)) ∘ (𝑓 ↾ (𝐴 ∖ (◡𝑓 “ ran 𝐸)))):(𝐴 ∖ (◡𝑓 “ ran 𝐸))–onto→ω) → ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
79 | 56, 77, 78 | sylancr 694 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
80 | | difexg 4735 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ V) |
81 | | isfin3-2 9072 |
. . . . . . . . . . 11
⊢ ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ V → ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬
ω ≼* (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
82 | 8, 80, 81 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝑓:𝐴–onto→ω → ((𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII ↔ ¬
ω ≼* (𝐴 ∖ (◡𝑓 “ ran 𝐸)))) |
83 | 82 | con2bid 343 |
. . . . . . . . 9
⊢ (𝑓:𝐴–onto→ω → (ω ≼*
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ↔ ¬ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
84 | 79, 83 | mpbid 221 |
. . . . . . . 8
⊢ (𝑓:𝐴–onto→ω → ¬ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII) |
85 | | eleq1 2676 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (𝑦 ∈ FinIII ↔ (◡𝑓 “ ran 𝐸) ∈
FinIII)) |
86 | | difeq2 3684 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (𝐴 ∖ 𝑦) = (𝐴 ∖ (◡𝑓 “ ran 𝐸))) |
87 | 86 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → ((𝐴 ∖ 𝑦) ∈ FinIII ↔ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
88 | 85, 87 | orbi12d 742 |
. . . . . . . . . . 11
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → ((𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ ((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
89 | 88 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ ¬
((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
90 | | ioran 510 |
. . . . . . . . . 10
⊢ (¬
((◡𝑓 “ ran 𝐸) ∈ FinIII ∨ (𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII) ↔ (¬
(◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII)) |
91 | 89, 90 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝑦 = (◡𝑓 “ ran 𝐸) → (¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) ↔ (¬
(◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈
FinIII))) |
92 | 91 | rspcev 3282 |
. . . . . . . 8
⊢ (((◡𝑓 “ ran 𝐸) ∈ 𝒫 𝐴 ∧ (¬ (◡𝑓 “ ran 𝐸) ∈ FinIII ∧ ¬
(𝐴 ∖ (◡𝑓 “ ran 𝐸)) ∈ FinIII)) →
∃𝑦 ∈ 𝒫
𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
93 | 13, 44, 84, 92 | syl12anc 1316 |
. . . . . . 7
⊢ (𝑓:𝐴–onto→ω → ∃𝑦 ∈ 𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
94 | | rexnal 2978 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝒫 𝐴 ¬ (𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈ FinIII)
↔ ¬ ∀𝑦
∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈
FinIII)) |
95 | 93, 94 | sylib 207 |
. . . . . 6
⊢ (𝑓:𝐴–onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
96 | 95 | exlimiv 1845 |
. . . . 5
⊢
(∃𝑓 𝑓:𝐴–onto→ω → ¬ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) |
97 | 4, 96 | sylbi 206 |
. . . 4
⊢ (ω
≼* 𝐴
→ ¬ ∀𝑦
∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈
FinIII)) |
98 | 97 | con2i 133 |
. . 3
⊢
(∀𝑦 ∈
𝒫 𝐴(𝑦 ∈ FinIII ∨
(𝐴 ∖ 𝑦) ∈ FinIII)
→ ¬ ω ≼* 𝐴) |
99 | | isfin3-2 9072 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinIII ↔ ¬
ω ≼* 𝐴)) |
100 | 98, 99 | syl5ibr 235 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII) → 𝐴 ∈
FinIII)) |
101 | 100 | imp 444 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦 ∈ 𝒫 𝐴(𝑦 ∈ FinIII ∨ (𝐴 ∖ 𝑦) ∈ FinIII)) → 𝐴 ∈
FinIII) |