Metamath Proof Explorer

Theorem infxpenc

Description: A canonical version of infxpen , by a completely different approach (although it uses infxpen via xpomen ). Using Cantor's normal form, we can show that A ^o B respects equinumerosity ( oef1o ), so that all the steps of (om ^ W ) x. ( om ^ W ) ~_om ^ ( 2 W ) ~ (om ^ 2 ) ^ W ~_om ^ W can be verified using bijections to do the ordinal commutations. (The assumption on N can be satisfied using cnfcom3c .) (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc.1 ⊢ φ → A ∈ On
infxpenc.2 ⊢ φ → ω ⊆ A
infxpenc.3 ⊢ φ → W ∈ On ∖ 1 𝑜
infxpenc.4 ⊢ φ → F : ω ↑ 𝑜 2 𝑜 ⟶ 1-1 onto ω
infxpenc.5 ⊢ φ → F ⁡ ∅ = ∅
infxpenc.6 ⊢ φ → N : A ⟶ 1-1 onto ω ↑ 𝑜 W
infxpenc.k ⊢ K = y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1
infxpenc.h ⊢ H = ω CNF W ∘ K ∘ ω ↑ 𝑜 2 𝑜 CNF W -1
infxpenc.l ⊢ L = y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ Y ∘ X -1 -1
infxpenc.x ⊢ X = z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w
infxpenc.y ⊢ Y = z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z
infxpenc.j ⊢ J = ω CNF 2 𝑜 ⋅ 𝑜 W ∘ L ∘ ω CNF W ⋅ 𝑜 2 𝑜 -1
infxpenc.z ⊢ Z = x ∈ ω ↑ 𝑜 W , y ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 x + 𝑜 y
infxpenc.t ⊢ T = x ∈ A , y ∈ A ⟼ N ⁡ x N ⁡ y
infxpenc.g ⊢ G = N -1 ∘ H ∘ J ∘ Z ∘ T
Assertion infxpenc ⊢ φ → G : A × A ⟶ 1-1 onto A

Proof

Step Hyp Ref Expression
1 infxpenc.1 ⊢ φ → A ∈ On
2 infxpenc.2 ⊢ φ → ω ⊆ A
3 infxpenc.3 ⊢ φ → W ∈ On ∖ 1 𝑜
4 infxpenc.4 ⊢ φ → F : ω ↑ 𝑜 2 𝑜 ⟶ 1-1 onto ω
5 infxpenc.5 ⊢ φ → F ⁡ ∅ = ∅
6 infxpenc.6 ⊢ φ → N : A ⟶ 1-1 onto ω ↑ 𝑜 W
7 infxpenc.k ⊢ K = y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1
8 infxpenc.h ⊢ H = ω CNF W ∘ K ∘ ω ↑ 𝑜 2 𝑜 CNF W -1
9 infxpenc.l ⊢ L = y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ Y ∘ X -1 -1
10 infxpenc.x ⊢ X = z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w
11 infxpenc.y ⊢ Y = z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z
12 infxpenc.j ⊢ J = ω CNF 2 𝑜 ⋅ 𝑜 W ∘ L ∘ ω CNF W ⋅ 𝑜 2 𝑜 -1
13 infxpenc.z ⊢ Z = x ∈ ω ↑ 𝑜 W , y ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 x + 𝑜 y
14 infxpenc.t ⊢ T = x ∈ A , y ∈ A ⟼ N ⁡ x N ⁡ y
15 infxpenc.g ⊢ G = N -1 ∘ H ∘ J ∘ Z ∘ T
16 f1ocnv ⊢ N : A ⟶ 1-1 onto ω ↑ 𝑜 W → N -1 : ω ↑ 𝑜 W ⟶ 1-1 onto A
17 6 16 syl ⊢ φ → N -1 : ω ↑ 𝑜 W ⟶ 1-1 onto A
18 f1oi ⊢ I ↾ W : W ⟶ 1-1 onto W
19 18 a1i ⊢ φ → I ↾ W : W ⟶ 1-1 onto W
20 omelon ⊢ ω ∈ On
21 20 a1i ⊢ φ → ω ∈ On
22 2on ⊢ 2 𝑜 ∈ On
23 oecl ⊢ ω ∈ On ∧ 2 𝑜 ∈ On → ω ↑ 𝑜 2 𝑜 ∈ On
24 21 22 23 sylancl ⊢ φ → ω ↑ 𝑜 2 𝑜 ∈ On
25 22 a1i ⊢ φ → 2 𝑜 ∈ On
26 peano1 ⊢ ∅ ∈ ω
27 26 a1i ⊢ φ → ∅ ∈ ω
28 oen0 ⊢ ω ∈ On ∧ 2 𝑜 ∈ On ∧ ∅ ∈ ω → ∅ ∈ ω ↑ 𝑜 2 𝑜
29 21 25 27 28 syl21anc ⊢ φ → ∅ ∈ ω ↑ 𝑜 2 𝑜
30 ondif1 ⊢ ω ↑ 𝑜 2 𝑜 ∈ On ∖ 1 𝑜 ↔ ω ↑ 𝑜 2 𝑜 ∈ On ∧ ∅ ∈ ω ↑ 𝑜 2 𝑜
31 24 29 30 sylanbrc ⊢ φ → ω ↑ 𝑜 2 𝑜 ∈ On ∖ 1 𝑜
32 3 eldifad ⊢ φ → W ∈ On
33 4 19 31 32 21 32 5 7 8 oef1o ⊢ φ → H : ω ↑ 𝑜 2 𝑜 ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W
34 f1oi ⊢ I ↾ ω : ω ⟶ 1-1 onto ω
35 34 a1i ⊢ φ → I ↾ ω : ω ⟶ 1-1 onto ω
36 10 11 omf1o ⊢ W ∈ On ∧ 2 𝑜 ∈ On → Y ∘ X -1 : W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto 2 𝑜 ⋅ 𝑜 W
37 32 22 36 sylancl ⊢ φ → Y ∘ X -1 : W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto 2 𝑜 ⋅ 𝑜 W
38 ondif1 ⊢ ω ∈ On ∖ 1 𝑜 ↔ ω ∈ On ∧ ∅ ∈ ω
39 20 26 38 mpbir2an ⊢ ω ∈ On ∖ 1 𝑜
40 39 a1i ⊢ φ → ω ∈ On ∖ 1 𝑜
41 omcl ⊢ W ∈ On ∧ 2 𝑜 ∈ On → W ⋅ 𝑜 2 𝑜 ∈ On
42 32 22 41 sylancl ⊢ φ → W ⋅ 𝑜 2 𝑜 ∈ On
43 omcl ⊢ 2 𝑜 ∈ On ∧ W ∈ On → 2 𝑜 ⋅ 𝑜 W ∈ On
44 25 32 43 syl2anc ⊢ φ → 2 𝑜 ⋅ 𝑜 W ∈ On
45 fvresi ⊢ ∅ ∈ ω → I ↾ ω ⁡ ∅ = ∅
46 26 45 mp1i ⊢ φ → I ↾ ω ⁡ ∅ = ∅
47 35 37 40 42 21 44 46 9 12 oef1o ⊢ φ → J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 2 𝑜 ⋅ 𝑜 W
48 oeoe ⊢ ω ∈ On ∧ 2 𝑜 ∈ On ∧ W ∈ On → ω ↑ 𝑜 2 𝑜 ↑ 𝑜 W = ω ↑ 𝑜 2 𝑜 ⋅ 𝑜 W
49 20 25 32 48 mp3an2i ⊢ φ → ω ↑ 𝑜 2 𝑜 ↑ 𝑜 W = ω ↑ 𝑜 2 𝑜 ⋅ 𝑜 W
50 49 f1oeq3d ⊢ φ → J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 2 𝑜 ↑ 𝑜 W ↔ J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 2 𝑜 ⋅ 𝑜 W
51 47 50 mpbird ⊢ φ → J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 2 𝑜 ↑ 𝑜 W
52 f1oco ⊢ H : ω ↑ 𝑜 2 𝑜 ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W ∧ J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 2 𝑜 ↑ 𝑜 W → H ∘ J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 W
53 33 51 52 syl2anc ⊢ φ → H ∘ J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 W
54 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
55 54 oveq2i ⊢ W ⋅ 𝑜 2 𝑜 = W ⋅ 𝑜 suc ⁡ 1 𝑜
56 1on ⊢ 1 𝑜 ∈ On
57 omsuc ⊢ W ∈ On ∧ 1 𝑜 ∈ On → W ⋅ 𝑜 suc ⁡ 1 𝑜 = W ⋅ 𝑜 1 𝑜 + 𝑜 W
58 32 56 57 sylancl ⊢ φ → W ⋅ 𝑜 suc ⁡ 1 𝑜 = W ⋅ 𝑜 1 𝑜 + 𝑜 W
59 55 58 syl5eq ⊢ φ → W ⋅ 𝑜 2 𝑜 = W ⋅ 𝑜 1 𝑜 + 𝑜 W
60 om1 ⊢ W ∈ On → W ⋅ 𝑜 1 𝑜 = W
61 32 60 syl ⊢ φ → W ⋅ 𝑜 1 𝑜 = W
62 61 oveq1d ⊢ φ → W ⋅ 𝑜 1 𝑜 + 𝑜 W = W + 𝑜 W
63 59 62 eqtrd ⊢ φ → W ⋅ 𝑜 2 𝑜 = W + 𝑜 W
64 63 oveq2d ⊢ φ → ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 = ω ↑ 𝑜 W + 𝑜 W
65 oeoa ⊢ ω ∈ On ∧ W ∈ On ∧ W ∈ On → ω ↑ 𝑜 W + 𝑜 W = ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W
66 20 32 32 65 mp3an2i ⊢ φ → ω ↑ 𝑜 W + 𝑜 W = ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W
67 64 66 eqtrd ⊢ φ → ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 = ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W
68 67 f1oeq2d ⊢ φ → H ∘ J : ω ↑ 𝑜 W ⋅ 𝑜 2 𝑜 ⟶ 1-1 onto ω ↑ 𝑜 W ↔ H ∘ J : ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W
69 53 68 mpbid ⊢ φ → H ∘ J : ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W
70 oecl ⊢ ω ∈ On ∧ W ∈ On → ω ↑ 𝑜 W ∈ On
71 21 32 70 syl2anc ⊢ φ → ω ↑ 𝑜 W ∈ On
72 13 omxpenlem ⊢ ω ↑ 𝑜 W ∈ On ∧ ω ↑ 𝑜 W ∈ On → Z : ω ↑ 𝑜 W × ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W
73 71 71 72 syl2anc ⊢ φ → Z : ω ↑ 𝑜 W × ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W
74 f1oco ⊢ H ∘ J : ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W ∧ Z : ω ↑ 𝑜 W × ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W ⋅ 𝑜 ω ↑ 𝑜 W → H ∘ J ∘ Z : ω ↑ 𝑜 W × ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W
75 69 73 74 syl2anc ⊢ φ → H ∘ J ∘ Z : ω ↑ 𝑜 W × ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W
76 f1of ⊢ N : A ⟶ 1-1 onto ω ↑ 𝑜 W → N : A ⟶ ω ↑ 𝑜 W
77 6 76 syl ⊢ φ → N : A ⟶ ω ↑ 𝑜 W
78 77 feqmptd ⊢ φ → N = x ∈ A ⟼ N ⁡ x
79 f1oeq1 ⊢ N = x ∈ A ⟼ N ⁡ x → N : A ⟶ 1-1 onto ω ↑ 𝑜 W ↔ x ∈ A ⟼ N ⁡ x : A ⟶ 1-1 onto ω ↑ 𝑜 W
80 78 79 syl ⊢ φ → N : A ⟶ 1-1 onto ω ↑ 𝑜 W ↔ x ∈ A ⟼ N ⁡ x : A ⟶ 1-1 onto ω ↑ 𝑜 W
81 6 80 mpbid ⊢ φ → x ∈ A ⟼ N ⁡ x : A ⟶ 1-1 onto ω ↑ 𝑜 W
82 77 feqmptd ⊢ φ → N = y ∈ A ⟼ N ⁡ y
83 f1oeq1 ⊢ N = y ∈ A ⟼ N ⁡ y → N : A ⟶ 1-1 onto ω ↑ 𝑜 W ↔ y ∈ A ⟼ N ⁡ y : A ⟶ 1-1 onto ω ↑ 𝑜 W
84 82 83 syl ⊢ φ → N : A ⟶ 1-1 onto ω ↑ 𝑜 W ↔ y ∈ A ⟼ N ⁡ y : A ⟶ 1-1 onto ω ↑ 𝑜 W
85 6 84 mpbid ⊢ φ → y ∈ A ⟼ N ⁡ y : A ⟶ 1-1 onto ω ↑ 𝑜 W
86 81 85 xpf1o ⊢ φ → x ∈ A , y ∈ A ⟼ N ⁡ x N ⁡ y : A × A ⟶ 1-1 onto ω ↑ 𝑜 W × ω ↑ 𝑜 W
87 f1oeq1 ⊢ T = x ∈ A , y ∈ A ⟼ N ⁡ x N ⁡ y → T : A × A ⟶ 1-1 onto ω ↑ 𝑜 W × ω ↑ 𝑜 W ↔ x ∈ A , y ∈ A ⟼ N ⁡ x N ⁡ y : A × A ⟶ 1-1 onto ω ↑ 𝑜 W × ω ↑ 𝑜 W
88 14 87 ax-mp ⊢ T : A × A ⟶ 1-1 onto ω ↑ 𝑜 W × ω ↑ 𝑜 W ↔ x ∈ A , y ∈ A ⟼ N ⁡ x N ⁡ y : A × A ⟶ 1-1 onto ω ↑ 𝑜 W × ω ↑ 𝑜 W
89 86 88 sylibr ⊢ φ → T : A × A ⟶ 1-1 onto ω ↑ 𝑜 W × ω ↑ 𝑜 W
90 f1oco ⊢ H ∘ J ∘ Z : ω ↑ 𝑜 W × ω ↑ 𝑜 W ⟶ 1-1 onto ω ↑ 𝑜 W ∧ T : A × A ⟶ 1-1 onto ω ↑ 𝑜 W × ω ↑ 𝑜 W → H ∘ J ∘ Z ∘ T : A × A ⟶ 1-1 onto ω ↑ 𝑜 W
91 75 89 90 syl2anc ⊢ φ → H ∘ J ∘ Z ∘ T : A × A ⟶ 1-1 onto ω ↑ 𝑜 W
92 f1oco ⊢ N -1 : ω ↑ 𝑜 W ⟶ 1-1 onto A ∧ H ∘ J ∘ Z ∘ T : A × A ⟶ 1-1 onto ω ↑ 𝑜 W → N -1 ∘ H ∘ J ∘ Z ∘ T : A × A ⟶ 1-1 onto A
93 17 91 92 syl2anc ⊢ φ → N -1 ∘ H ∘ J ∘ Z ∘ T : A × A ⟶ 1-1 onto A
94 f1oeq1 ⊢ G = N -1 ∘ H ∘ J ∘ Z ∘ T → G : A × A ⟶ 1-1 onto A ↔ N -1 ∘ H ∘ J ∘ Z ∘ T : A × A ⟶ 1-1 onto A
95 15 94 ax-mp ⊢ G : A × A ⟶ 1-1 onto A ↔ N -1 ∘ H ∘ J ∘ Z ∘ T : A × A ⟶ 1-1 onto A
96 93 95 sylibr ⊢ φ → G : A × A ⟶ 1-1 onto A