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 𝐸 )