Metamath Proof Explorer

Theorem fin1a2lem6

Description: Lemma for fin1a2 . Establish that _om can be broken into two equipollent 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 fin1a2lem6 ⊢S↾ran⁡E:ran⁡E⟶1-1 ontoω∖ran⁡E

Proof

Step Hyp Ref Expression
1 fin1a2lem.b ⊢E=x∈ω⟼2𝑜⋅𝑜x
2 fin1a2lem.aa ⊢S=x∈On⟼suc⁡x
3 2 fin1a2lem2 ⊢S:On⟶1-1On
4 1 fin1a2lem4 ⊢E:ω⟶1-1ω
5 f1f ⊢E:ω⟶1-1ω→E:ω⟶ω
6 frn ⊢E:ω⟶ω→ran⁡E⊆ω
7 omsson ⊢ω⊆On
8 6 7 sstrdi ⊢E:ω⟶ω→ran⁡E⊆On
9 4 5 8 mp2b ⊢ran⁡E⊆On
10 f1ores ⊢S:On⟶1-1On∧ran⁡E⊆On→S↾ran⁡E:ran⁡E⟶1-1 ontoSran⁡E
11 3 9 10 mp2an ⊢S↾ran⁡E:ran⁡E⟶1-1 ontoSran⁡E
12 9 sseli ⊢b∈ran⁡E→b∈On
13 2 fin1a2lem1 ⊢b∈On→S⁡b=suc⁡b
14 12 13 syl ⊢b∈ran⁡E→S⁡b=suc⁡b
15 14 eqeq1d ⊢b∈ran⁡E→S⁡b=a↔suc⁡b=a
16 15 rexbiia ⊢∃b∈ran⁡ES⁡b=a↔∃b∈ran⁡Esuc⁡b=a
17 4 5 6 mp2b ⊢ran⁡E⊆ω
18 17 sseli ⊢b∈ran⁡E→b∈ω
19 peano2 ⊢b∈ω→suc⁡b∈ω
20 18 19 syl ⊢b∈ran⁡E→suc⁡b∈ω
21 1 fin1a2lem5 ⊢b∈ω→b∈ran⁡E↔¬suc⁡b∈ran⁡E
22 21 biimpd ⊢b∈ω→b∈ran⁡E→¬suc⁡b∈ran⁡E
23 18 22 mpcom ⊢b∈ran⁡E→¬suc⁡b∈ran⁡E
24 20 23 jca ⊢b∈ran⁡E→suc⁡b∈ω∧¬suc⁡b∈ran⁡E
25 eleq1 ⊢suc⁡b=a→suc⁡b∈ω↔a∈ω
26 eleq1 ⊢suc⁡b=a→suc⁡b∈ran⁡E↔a∈ran⁡E
27 26 notbid ⊢suc⁡b=a→¬suc⁡b∈ran⁡E↔¬a∈ran⁡E
28 25 27 anbi12d ⊢suc⁡b=a→suc⁡b∈ω∧¬suc⁡b∈ran⁡E↔a∈ω∧¬a∈ran⁡E
29 24 28 syl5ibcom ⊢b∈ran⁡E→suc⁡b=a→a∈ω∧¬a∈ran⁡E
30 29 rexlimiv ⊢∃b∈ran⁡Esuc⁡b=a→a∈ω∧¬a∈ran⁡E
31 peano1 ⊢∅∈ω
32 1 fin1a2lem3 ⊢∅∈ω→E⁡∅=2𝑜⋅𝑜∅
33 31 32 ax-mp ⊢E⁡∅=2𝑜⋅𝑜∅
34 2on ⊢2𝑜∈On
35 om0 ⊢2𝑜∈On→2𝑜⋅𝑜∅=∅
36 34 35 ax-mp ⊢2𝑜⋅𝑜∅=∅
37 33 36 eqtri ⊢E⁡∅=∅
38 f1fun ⊢E:ω⟶1-1ω→Fun⁡E
39 4 38 ax-mp ⊢Fun⁡E
40 f1dm ⊢E:ω⟶1-1ω→dom⁡E=ω
41 4 40 ax-mp ⊢dom⁡E=ω
42 31 41 eleqtrri ⊢∅∈dom⁡E
43 fvelrn ⊢Fun⁡E∧∅∈dom⁡E→E⁡∅∈ran⁡E
44 39 42 43 mp2an ⊢E⁡∅∈ran⁡E
45 37 44 eqeltrri ⊢∅∈ran⁡E
46 eleq1 ⊢a=∅→a∈ran⁡E↔∅∈ran⁡E
47 45 46 mpbiri ⊢a=∅→a∈ran⁡E
48 47 necon3bi ⊢¬a∈ran⁡E→a≠∅
49 nnsuc ⊢a∈ω∧a≠∅→∃b∈ωa=suc⁡b
50 48 49 sylan2 ⊢a∈ω∧¬a∈ran⁡E→∃b∈ωa=suc⁡b
51 eleq1 ⊢a=suc⁡b→a∈ω↔suc⁡b∈ω
52 eleq1 ⊢a=suc⁡b→a∈ran⁡E↔suc⁡b∈ran⁡E
53 52 notbid ⊢a=suc⁡b→¬a∈ran⁡E↔¬suc⁡b∈ran⁡E
54 51 53 anbi12d ⊢a=suc⁡b→a∈ω∧¬a∈ran⁡E↔suc⁡b∈ω∧¬suc⁡b∈ran⁡E
55 54 anbi1d ⊢a=suc⁡b→a∈ω∧¬a∈ran⁡E∧b∈ω↔suc⁡b∈ω∧¬suc⁡b∈ran⁡E∧b∈ω
56 simplr ⊢suc⁡b∈ω∧¬suc⁡b∈ran⁡E∧b∈ω→¬suc⁡b∈ran⁡E
57 21 adantl ⊢suc⁡b∈ω∧¬suc⁡b∈ran⁡E∧b∈ω→b∈ran⁡E↔¬suc⁡b∈ran⁡E
58 56 57 mpbird ⊢suc⁡b∈ω∧¬suc⁡b∈ran⁡E∧b∈ω→b∈ran⁡E
59 55 58 syl6bi ⊢a=suc⁡b→a∈ω∧¬a∈ran⁡E∧b∈ω→b∈ran⁡E
60 59 com12 ⊢a∈ω∧¬a∈ran⁡E∧b∈ω→a=suc⁡b→b∈ran⁡E
61 60 impr ⊢a∈ω∧¬a∈ran⁡E∧b∈ω∧a=suc⁡b→b∈ran⁡E
62 simprr ⊢a∈ω∧¬a∈ran⁡E∧b∈ω∧a=suc⁡b→a=suc⁡b
63 62 eqcomd ⊢a∈ω∧¬a∈ran⁡E∧b∈ω∧a=suc⁡b→suc⁡b=a
64 50 61 63 reximssdv ⊢a∈ω∧¬a∈ran⁡E→∃b∈ran⁡Esuc⁡b=a
65 30 64 impbii ⊢∃b∈ran⁡Esuc⁡b=a↔a∈ω∧¬a∈ran⁡E
66 16 65 bitri ⊢∃b∈ran⁡ES⁡b=a↔a∈ω∧¬a∈ran⁡E
67 f1fn ⊢S:On⟶1-1On→SFnOn
68 3 67 ax-mp ⊢SFnOn
69 fvelimab ⊢SFnOn∧ran⁡E⊆On→a∈Sran⁡E↔∃b∈ran⁡ES⁡b=a
70 68 9 69 mp2an ⊢a∈Sran⁡E↔∃b∈ran⁡ES⁡b=a
71 eldif ⊢a∈ω∖ran⁡E↔a∈ω∧¬a∈ran⁡E
72 66 70 71 3bitr4i ⊢a∈Sran⁡E↔a∈ω∖ran⁡E
73 72 eqriv ⊢Sran⁡E=ω∖ran⁡E
74 f1oeq3 ⊢Sran⁡E=ω∖ran⁡E→S↾ran⁡E:ran⁡E⟶1-1 ontoSran⁡E↔S↾ran⁡E:ran⁡E⟶1-1 ontoω∖ran⁡E
75 73 74 ax-mp ⊢S↾ran⁡E:ran⁡E⟶1-1 ontoSran⁡E↔S↾ran⁡E:ran⁡E⟶1-1 ontoω∖ran⁡E
76 11 75 mpbi ⊢S↾ran⁡E:ran⁡E⟶1-1 ontoω∖ran⁡E