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 ⊢ 𝐸 = ( 𝑥 ∈ ω ↦ ( 2o ·o 𝑥 ) )
fin1a2lem.aa ⊢ 𝑆 = ( 𝑥 ∈ On ↦ suc 𝑥 )
Assertion fin1a2lem6 ( 𝑆 ↾ ran 𝐸 ) : ran 𝐸 –1-1-onto→ ( ω ∖ ran 𝐸 )

Proof

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