Metamath Proof Explorer

Theorem cnfcom3

Description: Any infinite ordinal B is equinumerous to a power of _om . (We are being careful here to show explicit bijections rather than simple equinumerosity because we want a uniform construction for cnfcom3c .) (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 4-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 𝐺 )
cnfcom3.1 ⊢ ( 𝜑 → ω ⊆ 𝐵 )
cnfcom.x ⊢ 𝑋 = ( 𝑢 ∈ ( 𝐹 ‘ 𝑊 ) , 𝑣 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( 𝐹 ‘ 𝑊 ) ·o 𝑣 ) +o 𝑢 ) )
cnfcom.y ⊢ 𝑌 = ( 𝑢 ∈ ( 𝐹 ‘ 𝑊 ) , 𝑣 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑢 ) +o 𝑣 ) )
cnfcom.n ⊢ 𝑁 = ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) )
Assertion cnfcom3 ( 𝜑 → 𝑁 : 𝐵 –1-1-onto→ ( ω ↑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 cnfcom3.1 ⊢ ( 𝜑 → ω ⊆ 𝐵 )
12 cnfcom.x ⊢ 𝑋 = ( 𝑢 ∈ ( 𝐹 ‘ 𝑊 ) , 𝑣 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( 𝐹 ‘ 𝑊 ) ·o 𝑣 ) +o 𝑢 ) )
13 cnfcom.y ⊢ 𝑌 = ( 𝑢 ∈ ( 𝐹 ‘ 𝑊 ) , 𝑣 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑢 ) +o 𝑣 ) )
14 cnfcom.n ⊢ 𝑁 = ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) )
15 omelon ⊢ ω ∈ On
16 suppssdm ⊢ ( 𝐹 supp ∅ ) ⊆ dom 𝐹
17 15 a1i ⊢ ( 𝜑 → ω ∈ On )
18 1 17 2 cantnff1o ⊢ ( 𝜑 → ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) )
19 f1ocnv ⊢ ( ( ω CNF 𝐴 ) : 𝑆 –1-1-onto→ ( ω ↑o 𝐴 ) → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 )
20 f1of ⊢ ( ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) –1-1-onto→ 𝑆 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
21 18 19 20 3syl ⊢ ( 𝜑 → ◡ ( ω CNF 𝐴 ) : ( ω ↑o 𝐴 ) ⟶ 𝑆 )
22 21 3 ffvelcdmd ⊢ ( 𝜑 → ( ◡ ( ω CNF 𝐴 ) ‘ 𝐵 ) ∈ 𝑆 )
23 4 22 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
24 1 17 2 cantnfs ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
25 23 24 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ω ∧ 𝐹 finSupp ∅ ) )
26 25 simpld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ω )
27 16 26 fssdm ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐴 )
28 ovex ⊢ ( 𝐹 supp ∅ ) ∈ V
29 5 oion ⊢ ( ( 𝐹 supp ∅ ) ∈ V → dom 𝐺 ∈ On )
30 28 29 ax-mp ⊢ dom 𝐺 ∈ On
31 30 elexi ⊢ dom 𝐺 ∈ V
32 31 uniex ⊢ ∪ dom 𝐺 ∈ V
33 32 sucid ⊢ ∪ dom 𝐺 ∈ suc ∪ dom 𝐺
34 peano1 ⊢ ∅ ∈ ω
35 34 a1i ⊢ ( 𝜑 → ∅ ∈ ω )
36 11 35 sseldd ⊢ ( 𝜑 → ∅ ∈ 𝐵 )
37 1 2 3 4 5 6 7 8 9 10 36 cnfcom2lem ⊢ ( 𝜑 → dom 𝐺 = suc ∪ dom 𝐺 )
38 33 37 eleqtrrid ⊢ ( 𝜑 → ∪ dom 𝐺 ∈ dom 𝐺 )
39 5 oif ⊢ 𝐺 : dom 𝐺 ⟶ ( 𝐹 supp ∅ )
40 39 ffvelcdmi ⊢ ( ∪ dom 𝐺 ∈ dom 𝐺 → ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ ( 𝐹 supp ∅ ) )
41 38 40 syl ⊢ ( 𝜑 → ( 𝐺 ‘ ∪ dom 𝐺 ) ∈ ( 𝐹 supp ∅ ) )
42 10 41 eqeltrid ⊢ ( 𝜑 → 𝑊 ∈ ( 𝐹 supp ∅ ) )
43 27 42 sseldd ⊢ ( 𝜑 → 𝑊 ∈ 𝐴 )
44 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑊 ∈ 𝐴 ) → 𝑊 ∈ On )
45 2 43 44 syl2anc ⊢ ( 𝜑 → 𝑊 ∈ On )
46 oecl ⊢ ( ( ω ∈ On ∧ 𝑊 ∈ On ) → ( ω ↑o 𝑊 ) ∈ On )
47 15 45 46 sylancr ⊢ ( 𝜑 → ( ω ↑o 𝑊 ) ∈ On )
48 26 43 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑊 ) ∈ ω )
49 nnon ⊢ ( ( 𝐹 ‘ 𝑊 ) ∈ ω → ( 𝐹 ‘ 𝑊 ) ∈ On )
50 48 49 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑊 ) ∈ On )
51 13 12 omf1o ⊢ ( ( ( ω ↑o 𝑊 ) ∈ On ∧ ( 𝐹 ‘ 𝑊 ) ∈ On ) → ( 𝑋 ∘ ◡ 𝑌 ) : ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ( 𝐹 ‘ 𝑊 ) ·o ( ω ↑o 𝑊 ) ) )
52 47 50 51 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∘ ◡ 𝑌 ) : ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ( 𝐹 ‘ 𝑊 ) ·o ( ω ↑o 𝑊 ) ) )
53 26 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
54 0ex ⊢ ∅ ∈ V
55 54 a1i ⊢ ( 𝜑 → ∅ ∈ V )
56 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ On ∧ ∅ ∈ V ) → ( 𝑊 ∈ ( 𝐹 supp ∅ ) ↔ ( 𝑊 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑊 ) ≠ ∅ ) ) )
57 53 2 55 56 syl3anc ⊢ ( 𝜑 → ( 𝑊 ∈ ( 𝐹 supp ∅ ) ↔ ( 𝑊 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑊 ) ≠ ∅ ) ) )
58 simpr ⊢ ( ( 𝑊 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑊 ) ≠ ∅ ) → ( 𝐹 ‘ 𝑊 ) ≠ ∅ )
59 57 58 biimtrdi ⊢ ( 𝜑 → ( 𝑊 ∈ ( 𝐹 supp ∅ ) → ( 𝐹 ‘ 𝑊 ) ≠ ∅ ) )
60 42 59 mpd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑊 ) ≠ ∅ )
61 on0eln0 ⊢ ( ( 𝐹 ‘ 𝑊 ) ∈ On → ( ∅ ∈ ( 𝐹 ‘ 𝑊 ) ↔ ( 𝐹 ‘ 𝑊 ) ≠ ∅ ) )
62 48 49 61 3syl ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐹 ‘ 𝑊 ) ↔ ( 𝐹 ‘ 𝑊 ) ≠ ∅ ) )
63 60 62 mpbird ⊢ ( 𝜑 → ∅ ∈ ( 𝐹 ‘ 𝑊 ) )
64 1 2 3 4 5 6 7 8 9 10 11 cnfcom3lem ⊢ ( 𝜑 → 𝑊 ∈ ( On ∖ 1o ) )
65 ondif1 ⊢ ( 𝑊 ∈ ( On ∖ 1o ) ↔ ( 𝑊 ∈ On ∧ ∅ ∈ 𝑊 ) )
66 65 simprbi ⊢ ( 𝑊 ∈ ( On ∖ 1o ) → ∅ ∈ 𝑊 )
67 64 66 syl ⊢ ( 𝜑 → ∅ ∈ 𝑊 )
68 omabs ⊢ ( ( ( ( 𝐹 ‘ 𝑊 ) ∈ ω ∧ ∅ ∈ ( 𝐹 ‘ 𝑊 ) ) ∧ ( 𝑊 ∈ On ∧ ∅ ∈ 𝑊 ) ) → ( ( 𝐹 ‘ 𝑊 ) ·o ( ω ↑o 𝑊 ) ) = ( ω ↑o 𝑊 ) )
69 48 63 45 67 68 syl22anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑊 ) ·o ( ω ↑o 𝑊 ) ) = ( ω ↑o 𝑊 ) )
70 69 f1oeq3d ⊢ ( 𝜑 → ( ( 𝑋 ∘ ◡ 𝑌 ) : ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ( 𝐹 ‘ 𝑊 ) ·o ( ω ↑o 𝑊 ) ) ↔ ( 𝑋 ∘ ◡ 𝑌 ) : ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) ) )
71 52 70 mpbid ⊢ ( 𝜑 → ( 𝑋 ∘ ◡ 𝑌 ) : ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) )
72 1 2 3 4 5 6 7 8 9 10 36 cnfcom2 ⊢ ( 𝜑 → ( 𝑇 ‘ dom 𝐺 ) : 𝐵 –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) )
73 f1oco ⊢ ( ( ( 𝑋 ∘ ◡ 𝑌 ) : ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) –1-1-onto→ ( ω ↑o 𝑊 ) ∧ ( 𝑇 ‘ dom 𝐺 ) : 𝐵 –1-1-onto→ ( ( ω ↑o 𝑊 ) ·o ( 𝐹 ‘ 𝑊 ) ) ) → ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) ) : 𝐵 –1-1-onto→ ( ω ↑o 𝑊 ) )
74 71 72 73 syl2anc ⊢ ( 𝜑 → ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) ) : 𝐵 –1-1-onto→ ( ω ↑o 𝑊 ) )
75 f1oeq1 ⊢ ( 𝑁 = ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) ) → ( 𝑁 : 𝐵 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) ) : 𝐵 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
76 14 75 ax-mp ⊢ ( 𝑁 : 𝐵 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) ) : 𝐵 –1-1-onto→ ( ω ↑o 𝑊 ) )
77 74 76 sylibr ⊢ ( 𝜑 → 𝑁 : 𝐵 –1-1-onto→ ( ω ↑o 𝑊 ) )