Metamath Proof Explorer

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 ( 𝐹 ‘ 𝑊 ) ) )