Theorem 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	27	f1oeq1d	⊢ ( 𝜑 → ( ( 𝑇 ‘ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) ↔ ( 𝑇 ‘ suc ∪ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) ) )
29	26 28	mpbird	⊢ ( 𝜑 → ( 𝑇 ‘ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) )
30		omelon	⊢ ω ∈ On
31	30	a1i	⊢ ( 𝜑 → ω ∈ On )
32	1 31 2	cantnff1o	⊢ ( 𝜑 → ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) )
33		f1ocnv	⊢ ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 )
34		f1of	⊢ ( ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
35	32 33 34	3syl	⊢ ( 𝜑 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
36	35 3	ffvelcdmd	⊢ ( 𝜑 → ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ∈ 𝑆 )
37	4 36	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
38	8	oveq1i	⊢ ( 𝑀 +o 𝑧 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 )
39	38	a1i	⊢ ( ( 𝑘 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑀 +o 𝑧 ) = ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) )
40	39	mpoeq3ia	⊢ ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) )
41		eqid	⊢ ∅ = ∅
42		seqomeq12	⊢ ( ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) = ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) ∧ ∅ = ∅ ) → seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
43	40 41 42	mp2an	⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
44	6 43	eqtri	⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
45	1 31 2 5 37 44	cantnfval	⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝐺 ) )
46	4	fveq2i	⊢ ( ( ω CNF 𝐴 ) ‘ 𝐹 ) = ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) )
47	45 46	eqtr3di	⊢ ( 𝜑 → ( 𝐻 ‘ dom 𝐺 ) = ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) )
48	18	fveq2d	⊢ ( 𝜑 → ( 𝐻 ‘ dom 𝐺 ) = ( 𝐻 ‘ suc ∪ dom 𝐺 ) )
49		f1ocnvfv2	⊢ ( ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) ∧ 𝐵 ∈ ( ω ↑o 𝐴 ) ) → ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
50	32 3 49	syl2anc	⊢ ( 𝜑 → ( ( ω CNF 𝐴 ) ‘ ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ) = 𝐵 )
51	47 48 50	3eqtr3d	⊢ ( 𝜑 → ( 𝐻 ‘ suc ∪ dom 𝐺 ) = 𝐵 )
52	51	f1oeq2d	⊢ ( 𝜑 → ( ( 𝑇 ‘ dom 𝐺 ) : ( 𝐻 ‘ suc ∪ dom 𝐺 ) –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) ↔ ( 𝑇 ‘ dom 𝐺 ) : 𝐵 –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) ) )
53	29 52	mpbid	⊢ ( 𝜑 → ( 𝑇 ‘ dom 𝐺 ) : 𝐵 –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) )