cnfcom2

Description: Any nonzero ordinal B is equinumerous to the leading term of its Cantor normal form. (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	cnfcom.s	⊢ 𝑆 = dom ( ω CNF 𝐴 )
	cnfcom.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cnfcom.b	⊢ ( 𝜑 → 𝐵 ∈ ( ω ↑_o 𝐴 ) )
	cnfcom.f	⊢ 𝐹 = ( ^◡ ( ω CNF 𝐴 ) ‘ 𝐵 )
	cnfcom.g	⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
	cnfcom.h	⊢ 𝐻 = seq_ω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +_o 𝑧 ) ) , ∅ )
	cnfcom.t	⊢ 𝑇 = seq_ω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) , ∅ )
	cnfcom.m	⊢ 𝑀 = ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
	cnfcom.k	⊢ 𝐾 = ( ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +_o 𝑥 ) ) ∪ ^◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +_o 𝑥 ) ) )
	cnfcom.w	⊢ 𝑊 = ( 𝐺 ‘ ∪ dom 𝐺 )
	cnfcom2.1	⊢ ( 𝜑 → ∅ ∈ 𝐵 )
Assertion	cnfcom2	⊢ ( 𝜑 → ( 𝑇 ‘ dom 𝐺 ) : 𝐵 –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnfcom.s	⊢ 𝑆 = dom ( ω CNF 𝐴 )
2		cnfcom.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cnfcom.b	⊢ ( 𝜑 → 𝐵 ∈ ( ω ↑_o 𝐴 ) )
4		cnfcom.f	⊢ 𝐹 = ( ^◡ ( ω CNF 𝐴 ) ‘ 𝐵 )
5		cnfcom.g	⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
6		cnfcom.h	⊢ 𝐻 = seq_ω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +_o 𝑧 ) ) , ∅ )
7		cnfcom.t	⊢ 𝑇 = seq_ω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) , ∅ )
8		cnfcom.m	⊢ 𝑀 = ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
9		cnfcom.k	⊢ 𝐾 = ( ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +_o 𝑥 ) ) ∪ ^◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +_o 𝑥 ) ) )
10		cnfcom.w	⊢ 𝑊 = ( 𝐺 ‘ ∪ dom 𝐺 )
11		cnfcom2.1	⊢ ( 𝜑 → ∅ ∈ 𝐵 )
12		ovex	⊢ ( 𝐹 supp ∅ ) ∈ V
13	5	oion	⊢ ( ( 𝐹 supp ∅ ) ∈ V → dom 𝐺 ∈ On )
14	12 13	ax-mp	⊢ dom 𝐺 ∈ On
15	14	elexi	⊢ dom 𝐺 ∈ V
16	15	uniex	⊢ ∪ dom 𝐺 ∈ V
17	16	sucid	⊢ ∪ dom 𝐺 ∈ suc ∪ dom 𝐺
18	1 2 3 4 5 6 7 8 9 10 11	cnfcom2lem	⊢ ( 𝜑 → dom 𝐺 = suc ∪ dom 𝐺 )
19	17 18	eleqtrrid	⊢ ( 𝜑 → ∪ dom 𝐺 ∈ dom 𝐺 )
20	1 2 3 4 5 6 7 8 9 19	cnfcom	⊢ ( 𝜑 → ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o ( 𝐺 ‘ ∪ dom 𝐺 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ ∪ dom 𝐺 ) ) ) )
21	10	oveq2i	⊢ ( ω ↑_o 𝑊 ) = ( ω ↑_o ( 𝐺 ‘ ∪ dom 𝐺 ) )
22	10	fveq2i	⊢ ( 𝐹 ‘ 𝑊 ) = ( 𝐹 ‘ ( 𝐺 ‘ ∪ dom 𝐺 ) )
23	21 22	oveq12i	⊢ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) = ( ( ω ↑_o ( 𝐺 ‘ ∪ dom 𝐺 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ ∪ dom 𝐺 ) ) )
24		f1oeq3	⊢ ( ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) = ( ( ω ↑_o ( 𝐺 ‘ ∪ dom 𝐺 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ ∪ dom 𝐺 ) ) ) → ( ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ↔ ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o ( 𝐺 ‘ ∪ dom 𝐺 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ ∪ dom 𝐺 ) ) ) ) )
25	23 24	ax-mp	⊢ ( ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ↔ ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o ( 𝐺 ‘ ∪ dom 𝐺 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ ∪ dom 𝐺 ) ) ) )
26	20 25	sylibr	⊢ ( 𝜑 → ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) )
27	18	fveq2d	⊢ ( 𝜑 → ( 𝑇 ‘ dom 𝐺 ) = ( 𝑇 ‘ suc ∪ dom 𝐺 ) )
28		f1oeq1	⊢ ( ( 𝑇 ‘ dom 𝐺 ) = ( 𝑇 ‘ suc ∪ dom 𝐺 ) → ( ( 𝑇 ‘ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ↔ ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ) )
29	27 28	syl	⊢ ( 𝜑 → ( ( 𝑇 ‘ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ↔ ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ) )
30	26 29	mpbird	⊢ ( 𝜑 → ( 𝑇 ‘ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) )
31	4	fveq2i	⊢ ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = ( ( ω CNF 𝐴 ) ‘ ( ^◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) )
32		omelon	⊢ ω ∈ On
33	32	a1i	⊢ ( 𝜑 → ω ∈ On )
34	1 33 2	cantnff1o	⊢ ( 𝜑 → ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑_o 𝐴 ) )
35		f1ocnv	⊢ ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑_o 𝐴 ) → ^◡ ( ω CNF 𝐴 ) : ( ω ↑_o 𝐴 ) –1-1-onto→ 𝑆 )
36		f1of	⊢ ( ^◡ ( ω CNF 𝐴 ) : ( ω ↑_o 𝐴 ) –1-1-onto→ 𝑆 → ^◡ ( ω CNF 𝐴 ) : ( ω ↑_o 𝐴 ) ⟶ 𝑆 )
37	34 35 36	3syl	⊢ ( 𝜑 → ^◡ ( ω CNF 𝐴 ) : ( ω ↑_o 𝐴 ) ⟶ 𝑆 )
38	37 3	ffvelrnd	⊢ ( 𝜑 → ( ^◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ∈ 𝑆 )
39	4 38	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
40	8	oveq1i	⊢ ( 𝑀 +_o 𝑧 ) = ( ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +_o 𝑧 )
41	40	a1i	⊢ ( ( 𝑘 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑀 +_o 𝑧 ) = ( ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +_o 𝑧 ) )
42	41	mpoeq3ia	⊢ ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +_o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +_o 𝑧 ) )
43		eqid	⊢ ∅ = ∅
44		seqomeq12	⊢ ( ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +_o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +_o 𝑧 ) ) ∧ ∅ = ∅ ) → seq_ω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +_o 𝑧 ) ) , ∅ ) = seq_ω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +_o 𝑧 ) ) , ∅ ) )
45	42 43 44	mp2an	⊢ seq_ω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +_o 𝑧 ) ) , ∅ ) = seq_ω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +_o 𝑧 ) ) , ∅ )
46	6 45	eqtri	⊢ 𝐻 = seq_ω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑_o ( 𝐺 ‘ 𝑘 ) ) ·_o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +_o 𝑧 ) ) , ∅ )
47	1 33 2 5 39 46	cantnfval	⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )
48	31 47	syl5reqr	⊢ ( 𝜑 → ( 𝐻 ‘ dom 𝐺 ) = ( ( ω CNF 𝐴 ) ‘ ( ^◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) )
49	18	fveq2d	⊢ ( 𝜑 → ( 𝐻 ‘ dom 𝐺 ) = ( 𝐻 ‘ suc ∪ dom 𝐺 ) )
50		f1ocnvfv2	⊢ ( ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑_o 𝐴 ) ∧ 𝐵 ∈ ( ω ↑_o 𝐴 ) ) → ( ( ω CNF 𝐴 ) ‘ ( ^◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
51	34 3 50	syl2anc	⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ ( ^◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
52	48 49 51	3eqtr3d	⊢ ( 𝜑 → ( 𝐻 ‘ suc ∪ dom 𝐺 ) = 𝐵 )
53	52	f1oeq2d	⊢ ( 𝜑 → ( ( 𝑇 ‘ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ↔ ( 𝑇 ‘ dom 𝐺 ) : 𝐵 –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) ) )
54	30 53	mpbid	⊢ ( 𝜑 → ( 𝑇 ‘ dom 𝐺 ) : 𝐵 –1-1-onto→ ( ( ω ↑_o 𝑊 ) ·_o ( 𝐹 ‘ 𝑊 ) ) )

Metamath Proof Explorer

Theorem cnfcom2

Proof