Metamath Proof Explorer

Theorem fin1a2lem7

Description: Lemma for fin1a2 . Split a III-infinite set in two pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

Ref Expression
Hypotheses fin1a2lem.b ⊢ E = x ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 x
fin1a2lem.aa ⊢ S = x ∈ On ⟼ suc ⁡ x
Assertion fin1a2lem7 ⊢ A ∈ V ∧ ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII → A ∈ FinIII

Proof

Step Hyp Ref Expression
1 fin1a2lem.b ⊢ E = x ∈ ω ⟼ 2 𝑜 ⋅ 𝑜 x
2 fin1a2lem.aa ⊢ S = x ∈ On ⟼ suc ⁡ x
3 peano1 ⊢ ∅ ∈ ω
4 ne0i ⊢ ∅ ∈ ω → ω ≠ ∅
5 brwdomn0 ⊢ ω ≠ ∅ → ω ≼ * A ↔ ∃ f f : A ⟶ onto ω
6 3 4 5 mp2b ⊢ ω ≼ * A ↔ ∃ f f : A ⟶ onto ω
7 vex ⊢ f ∈ V
8 fof ⊢ f : A ⟶ onto ω → f : A ⟶ ω
9 dmfex ⊢ f ∈ V ∧ f : A ⟶ ω → A ∈ V
10 7 8 9 sylancr ⊢ f : A ⟶ onto ω → A ∈ V
11 cnvimass ⊢ f -1 ran ⁡ E ⊆ dom ⁡ f
12 11 8 fssdm ⊢ f : A ⟶ onto ω → f -1 ran ⁡ E ⊆ A
13 10 12 sselpwd ⊢ f : A ⟶ onto ω → f -1 ran ⁡ E ∈ 𝒫 A
14 1 fin1a2lem4 ⊢ E : ω ⟶ 1-1 ω
15 f1cnv ⊢ E : ω ⟶ 1-1 ω → E -1 : ran ⁡ E ⟶ 1-1 onto ω
16 f1ofo ⊢ E -1 : ran ⁡ E ⟶ 1-1 onto ω → E -1 : ran ⁡ E ⟶ onto ω
17 14 15 16 mp2b ⊢ E -1 : ran ⁡ E ⟶ onto ω
18 fofun ⊢ E -1 : ran ⁡ E ⟶ onto ω → Fun ⁡ E -1
19 17 18 ax-mp ⊢ Fun ⁡ E -1
20 7 resex ⊢ f ↾ f -1 ran ⁡ E ∈ V
21 cofunexg ⊢ Fun ⁡ E -1 ∧ f ↾ f -1 ran ⁡ E ∈ V → E -1 ∘ f ↾ f -1 ran ⁡ E ∈ V
22 19 20 21 mp2an ⊢ E -1 ∘ f ↾ f -1 ran ⁡ E ∈ V
23 fofun ⊢ f : A ⟶ onto ω → Fun ⁡ f
24 fores ⊢ Fun ⁡ f ∧ f -1 ran ⁡ E ⊆ dom ⁡ f → f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto f f -1 ran ⁡ E
25 23 11 24 sylancl ⊢ f : A ⟶ onto ω → f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto f f -1 ran ⁡ E
26 f1f ⊢ E : ω ⟶ 1-1 ω → E : ω ⟶ ω
27 frn ⊢ E : ω ⟶ ω → ran ⁡ E ⊆ ω
28 14 26 27 mp2b ⊢ ran ⁡ E ⊆ ω
29 foimacnv ⊢ f : A ⟶ onto ω ∧ ran ⁡ E ⊆ ω → f f -1 ran ⁡ E = ran ⁡ E
30 28 29 mpan2 ⊢ f : A ⟶ onto ω → f f -1 ran ⁡ E = ran ⁡ E
31 foeq3 ⊢ f f -1 ran ⁡ E = ran ⁡ E → f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto f f -1 ran ⁡ E ↔ f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto ran ⁡ E
32 30 31 syl ⊢ f : A ⟶ onto ω → f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto f f -1 ran ⁡ E ↔ f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto ran ⁡ E
33 25 32 mpbid ⊢ f : A ⟶ onto ω → f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto ran ⁡ E
34 foco ⊢ E -1 : ran ⁡ E ⟶ onto ω ∧ f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto ran ⁡ E → E -1 ∘ f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto ω
35 17 33 34 sylancr ⊢ f : A ⟶ onto ω → E -1 ∘ f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto ω
36 fowdom ⊢ E -1 ∘ f ↾ f -1 ran ⁡ E ∈ V ∧ E -1 ∘ f ↾ f -1 ran ⁡ E : f -1 ran ⁡ E ⟶ onto ω → ω ≼ * f -1 ran ⁡ E
37 22 35 36 sylancr ⊢ f : A ⟶ onto ω → ω ≼ * f -1 ran ⁡ E
38 7 cnvex ⊢ f -1 ∈ V
39 38 imaex ⊢ f -1 ran ⁡ E ∈ V
40 isfin3-2 ⊢ f -1 ran ⁡ E ∈ V → f -1 ran ⁡ E ∈ FinIII ↔ ¬ ω ≼ * f -1 ran ⁡ E
41 39 40 ax-mp ⊢ f -1 ran ⁡ E ∈ FinIII ↔ ¬ ω ≼ * f -1 ran ⁡ E
42 41 con2bii ⊢ ω ≼ * f -1 ran ⁡ E ↔ ¬ f -1 ran ⁡ E ∈ FinIII
43 37 42 sylib ⊢ f : A ⟶ onto ω → ¬ f -1 ran ⁡ E ∈ FinIII
44 1 2 fin1a2lem6 ⊢ S ↾ ran ⁡ E : ran ⁡ E ⟶ 1-1 onto ω ∖ ran ⁡ E
45 f1ocnv ⊢ S ↾ ran ⁡ E : ran ⁡ E ⟶ 1-1 onto ω ∖ ran ⁡ E → S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ 1-1 onto ran ⁡ E
46 f1ofo ⊢ S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ 1-1 onto ran ⁡ E → S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ onto ran ⁡ E
47 44 45 46 mp2b ⊢ S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ onto ran ⁡ E
48 foco ⊢ E -1 : ran ⁡ E ⟶ onto ω ∧ S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ onto ran ⁡ E → E -1 ∘ S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ onto ω
49 17 47 48 mp2an ⊢ E -1 ∘ S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ onto ω
50 fofun ⊢ E -1 ∘ S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ onto ω → Fun ⁡ E -1 ∘ S ↾ ran ⁡ E -1
51 49 50 ax-mp ⊢ Fun ⁡ E -1 ∘ S ↾ ran ⁡ E -1
52 7 resex ⊢ f ↾ A ∖ f -1 ran ⁡ E ∈ V
53 cofunexg ⊢ Fun ⁡ E -1 ∘ S ↾ ran ⁡ E -1 ∧ f ↾ A ∖ f -1 ran ⁡ E ∈ V → E -1 ∘ S ↾ ran ⁡ E -1 ∘ f ↾ A ∖ f -1 ran ⁡ E ∈ V
54 51 52 53 mp2an ⊢ E -1 ∘ S ↾ ran ⁡ E -1 ∘ f ↾ A ∖ f -1 ran ⁡ E ∈ V
55 difss ⊢ A ∖ f -1 ran ⁡ E ⊆ A
56 8 fdmd ⊢ f : A ⟶ onto ω → dom ⁡ f = A
57 55 56 sseqtrrid ⊢ f : A ⟶ onto ω → A ∖ f -1 ran ⁡ E ⊆ dom ⁡ f
58 fores ⊢ Fun ⁡ f ∧ A ∖ f -1 ran ⁡ E ⊆ dom ⁡ f → f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto f A ∖ f -1 ran ⁡ E
59 23 57 58 syl2anc ⊢ f : A ⟶ onto ω → f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto f A ∖ f -1 ran ⁡ E
60 funcnvcnv ⊢ Fun ⁡ f → Fun ⁡ f -1 -1
61 imadif ⊢ Fun ⁡ f -1 -1 → f -1 ω ∖ ran ⁡ E = f -1 ω ∖ f -1 ran ⁡ E
62 23 60 61 3syl ⊢ f : A ⟶ onto ω → f -1 ω ∖ ran ⁡ E = f -1 ω ∖ f -1 ran ⁡ E
63 62 imaeq2d ⊢ f : A ⟶ onto ω → f f -1 ω ∖ ran ⁡ E = f f -1 ω ∖ f -1 ran ⁡ E
64 difss ⊢ ω ∖ ran ⁡ E ⊆ ω
65 foimacnv ⊢ f : A ⟶ onto ω ∧ ω ∖ ran ⁡ E ⊆ ω → f f -1 ω ∖ ran ⁡ E = ω ∖ ran ⁡ E
66 64 65 mpan2 ⊢ f : A ⟶ onto ω → f f -1 ω ∖ ran ⁡ E = ω ∖ ran ⁡ E
67 fimacnv ⊢ f : A ⟶ ω → f -1 ω = A
68 8 67 syl ⊢ f : A ⟶ onto ω → f -1 ω = A
69 68 difeq1d ⊢ f : A ⟶ onto ω → f -1 ω ∖ f -1 ran ⁡ E = A ∖ f -1 ran ⁡ E
70 69 imaeq2d ⊢ f : A ⟶ onto ω → f f -1 ω ∖ f -1 ran ⁡ E = f A ∖ f -1 ran ⁡ E
71 63 66 70 3eqtr3rd ⊢ f : A ⟶ onto ω → f A ∖ f -1 ran ⁡ E = ω ∖ ran ⁡ E
72 foeq3 ⊢ f A ∖ f -1 ran ⁡ E = ω ∖ ran ⁡ E → f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto f A ∖ f -1 ran ⁡ E ↔ f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto ω ∖ ran ⁡ E
73 71 72 syl ⊢ f : A ⟶ onto ω → f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto f A ∖ f -1 ran ⁡ E ↔ f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto ω ∖ ran ⁡ E
74 59 73 mpbid ⊢ f : A ⟶ onto ω → f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto ω ∖ ran ⁡ E
75 foco ⊢ E -1 ∘ S ↾ ran ⁡ E -1 : ω ∖ ran ⁡ E ⟶ onto ω ∧ f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto ω ∖ ran ⁡ E → E -1 ∘ S ↾ ran ⁡ E -1 ∘ f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto ω
76 49 74 75 sylancr ⊢ f : A ⟶ onto ω → E -1 ∘ S ↾ ran ⁡ E -1 ∘ f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto ω
77 fowdom ⊢ E -1 ∘ S ↾ ran ⁡ E -1 ∘ f ↾ A ∖ f -1 ran ⁡ E ∈ V ∧ E -1 ∘ S ↾ ran ⁡ E -1 ∘ f ↾ A ∖ f -1 ran ⁡ E : A ∖ f -1 ran ⁡ E ⟶ onto ω → ω ≼ * A ∖ f -1 ran ⁡ E
78 54 76 77 sylancr ⊢ f : A ⟶ onto ω → ω ≼ * A ∖ f -1 ran ⁡ E
79 difexg ⊢ A ∈ V → A ∖ f -1 ran ⁡ E ∈ V
80 isfin3-2 ⊢ A ∖ f -1 ran ⁡ E ∈ V → A ∖ f -1 ran ⁡ E ∈ FinIII ↔ ¬ ω ≼ * A ∖ f -1 ran ⁡ E
81 10 79 80 3syl ⊢ f : A ⟶ onto ω → A ∖ f -1 ran ⁡ E ∈ FinIII ↔ ¬ ω ≼ * A ∖ f -1 ran ⁡ E
82 81 con2bid ⊢ f : A ⟶ onto ω → ω ≼ * A ∖ f -1 ran ⁡ E ↔ ¬ A ∖ f -1 ran ⁡ E ∈ FinIII
83 78 82 mpbid ⊢ f : A ⟶ onto ω → ¬ A ∖ f -1 ran ⁡ E ∈ FinIII
84 eleq1 ⊢ y = f -1 ran ⁡ E → y ∈ FinIII ↔ f -1 ran ⁡ E ∈ FinIII
85 difeq2 ⊢ y = f -1 ran ⁡ E → A ∖ y = A ∖ f -1 ran ⁡ E
86 85 eleq1d ⊢ y = f -1 ran ⁡ E → A ∖ y ∈ FinIII ↔ A ∖ f -1 ran ⁡ E ∈ FinIII
87 84 86 orbi12d ⊢ y = f -1 ran ⁡ E → y ∈ FinIII ∨ A ∖ y ∈ FinIII ↔ f -1 ran ⁡ E ∈ FinIII ∨ A ∖ f -1 ran ⁡ E ∈ FinIII
88 87 notbid ⊢ y = f -1 ran ⁡ E → ¬ y ∈ FinIII ∨ A ∖ y ∈ FinIII ↔ ¬ f -1 ran ⁡ E ∈ FinIII ∨ A ∖ f -1 ran ⁡ E ∈ FinIII
89 ioran ⊢ ¬ f -1 ran ⁡ E ∈ FinIII ∨ A ∖ f -1 ran ⁡ E ∈ FinIII ↔ ¬ f -1 ran ⁡ E ∈ FinIII ∧ ¬ A ∖ f -1 ran ⁡ E ∈ FinIII
90 88 89 bitrdi ⊢ y = f -1 ran ⁡ E → ¬ y ∈ FinIII ∨ A ∖ y ∈ FinIII ↔ ¬ f -1 ran ⁡ E ∈ FinIII ∧ ¬ A ∖ f -1 ran ⁡ E ∈ FinIII
91 90 rspcev ⊢ f -1 ran ⁡ E ∈ 𝒫 A ∧ ¬ f -1 ran ⁡ E ∈ FinIII ∧ ¬ A ∖ f -1 ran ⁡ E ∈ FinIII → ∃ y ∈ 𝒫 A ¬ y ∈ FinIII ∨ A ∖ y ∈ FinIII
92 13 43 83 91 syl12anc ⊢ f : A ⟶ onto ω → ∃ y ∈ 𝒫 A ¬ y ∈ FinIII ∨ A ∖ y ∈ FinIII
93 rexnal ⊢ ∃ y ∈ 𝒫 A ¬ y ∈ FinIII ∨ A ∖ y ∈ FinIII ↔ ¬ ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII
94 92 93 sylib ⊢ f : A ⟶ onto ω → ¬ ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII
95 94 exlimiv ⊢ ∃ f f : A ⟶ onto ω → ¬ ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII
96 6 95 sylbi ⊢ ω ≼ * A → ¬ ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII
97 96 con2i ⊢ ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII → ¬ ω ≼ * A
98 isfin3-2 ⊢ A ∈ V → A ∈ FinIII ↔ ¬ ω ≼ * A
99 97 98 imbitrrid ⊢ A ∈ V → ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII → A ∈ FinIII
100 99 imp ⊢ A ∈ V ∧ ∀ y ∈ 𝒫 A y ∈ FinIII ∨ A ∖ y ∈ FinIII → A ∈ FinIII