Metamath Proof Explorer


Theorem cantnf

Description: The Cantor Normal Form theorem. The function ( A CNF B ) , which maps a finitely supported function from B to A to the sum ( ( A ^o f ( a 1 ) ) o. a 1 ) +o ( ( A ^o f ( a 2 ) ) o. a 2 ) +o ... over all indices a < B such that f ( a ) is nonzero, is an order isomorphism from the ordering T of finitely supported functions to the set ( A ^o B ) under the natural order. Setting A = _om and letting B be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres , implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s S = dom A CNF B
cantnfs.a φ A On
cantnfs.b φ B On
oemapval.t T = x y | z B x z y z w B z w x w = y w
Assertion cantnf φ A CNF B Isom T , E S A 𝑜 B

Proof

Step Hyp Ref Expression
1 cantnfs.s S = dom A CNF B
2 cantnfs.a φ A On
3 cantnfs.b φ B On
4 oemapval.t T = x y | z B x z y z w B z w x w = y w
5 1 2 3 4 oemapso φ T Or S
6 oecl A On B On A 𝑜 B On
7 2 3 6 syl2anc φ A 𝑜 B On
8 eloni A 𝑜 B On Ord A 𝑜 B
9 7 8 syl φ Ord A 𝑜 B
10 ordwe Ord A 𝑜 B E We A 𝑜 B
11 weso E We A 𝑜 B E Or A 𝑜 B
12 sopo E Or A 𝑜 B E Po A 𝑜 B
13 9 10 11 12 4syl φ E Po A 𝑜 B
14 1 2 3 cantnff φ A CNF B : S A 𝑜 B
15 14 frnd φ ran A CNF B A 𝑜 B
16 onss A 𝑜 B On A 𝑜 B On
17 7 16 syl φ A 𝑜 B On
18 17 sseld φ t A 𝑜 B t On
19 eleq1w t = y t A 𝑜 B y A 𝑜 B
20 eleq1w t = y t ran A CNF B y ran A CNF B
21 19 20 imbi12d t = y t A 𝑜 B t ran A CNF B y A 𝑜 B y ran A CNF B
22 21 imbi2d t = y φ t A 𝑜 B t ran A CNF B φ y A 𝑜 B y ran A CNF B
23 r19.21v y t φ y A 𝑜 B y ran A CNF B φ y t y A 𝑜 B y ran A CNF B
24 ordelss Ord A 𝑜 B t A 𝑜 B t A 𝑜 B
25 9 24 sylan φ t A 𝑜 B t A 𝑜 B
26 25 sselda φ t A 𝑜 B y t y A 𝑜 B
27 pm5.5 y A 𝑜 B y A 𝑜 B y ran A CNF B y ran A CNF B
28 26 27 syl φ t A 𝑜 B y t y A 𝑜 B y ran A CNF B y ran A CNF B
29 28 ralbidva φ t A 𝑜 B y t y A 𝑜 B y ran A CNF B y t y ran A CNF B
30 dfss3 t ran A CNF B y t y ran A CNF B
31 29 30 bitr4di φ t A 𝑜 B y t y A 𝑜 B y ran A CNF B t ran A CNF B
32 eleq1 t = t ran A CNF B ran A CNF B
33 2 adantr φ t A 𝑜 B t ran A CNF B A On
34 33 adantr φ t A 𝑜 B t ran A CNF B t A On
35 3 adantr φ t A 𝑜 B t ran A CNF B B On
36 35 adantr φ t A 𝑜 B t ran A CNF B t B On
37 simplrl φ t A 𝑜 B t ran A CNF B t t A 𝑜 B
38 simplrr φ t A 𝑜 B t ran A CNF B t t ran A CNF B
39 7 adantr φ t A 𝑜 B t ran A CNF B A 𝑜 B On
40 simprl φ t A 𝑜 B t ran A CNF B t A 𝑜 B
41 onelon A 𝑜 B On t A 𝑜 B t On
42 39 40 41 syl2anc φ t A 𝑜 B t ran A CNF B t On
43 on0eln0 t On t t
44 42 43 syl φ t A 𝑜 B t ran A CNF B t t
45 44 biimpar φ t A 𝑜 B t ran A CNF B t t
46 eqid c On | t A 𝑜 c = c On | t A 𝑜 c
47 eqid ι d | a On b A 𝑜 c On | t A 𝑜 c d = a b A 𝑜 c On | t A 𝑜 c 𝑜 a + 𝑜 b = t = ι d | a On b A 𝑜 c On | t A 𝑜 c d = a b A 𝑜 c On | t A 𝑜 c 𝑜 a + 𝑜 b = t
48 eqid 1 st ι d | a On b A 𝑜 c On | t A 𝑜 c d = a b A 𝑜 c On | t A 𝑜 c 𝑜 a + 𝑜 b = t = 1 st ι d | a On b A 𝑜 c On | t A 𝑜 c d = a b A 𝑜 c On | t A 𝑜 c 𝑜 a + 𝑜 b = t
49 eqid 2 nd ι d | a On b A 𝑜 c On | t A 𝑜 c d = a b A 𝑜 c On | t A 𝑜 c 𝑜 a + 𝑜 b = t = 2 nd ι d | a On b A 𝑜 c On | t A 𝑜 c d = a b A 𝑜 c On | t A 𝑜 c 𝑜 a + 𝑜 b = t
50 1 34 36 4 37 38 45 46 47 48 49 cantnflem4 φ t A 𝑜 B t ran A CNF B t t ran A CNF B
51 fczsupp0 B × supp =
52 51 eqcomi = B × supp
53 oieq2 = B × supp OrdIso E = OrdIso E B × supp
54 52 53 ax-mp OrdIso E = OrdIso E B × supp
55 ne0i t A 𝑜 B A 𝑜 B
56 55 ad2antrl φ t A 𝑜 B t ran A CNF B A 𝑜 B
57 oveq1 A = A 𝑜 B = 𝑜 B
58 57 neeq1d A = A 𝑜 B 𝑜 B
59 56 58 syl5ibcom φ t A 𝑜 B t ran A CNF B A = 𝑜 B
60 59 necon2d φ t A 𝑜 B t ran A CNF B 𝑜 B = A
61 on0eln0 B On B B
62 oe0m1 B On B 𝑜 B =
63 61 62 bitr3d B On B 𝑜 B =
64 35 63 syl φ t A 𝑜 B t ran A CNF B B 𝑜 B =
65 on0eln0 A On A A
66 33 65 syl φ t A 𝑜 B t ran A CNF B A A
67 60 64 66 3imtr4d φ t A 𝑜 B t ran A CNF B B A
68 ne0i y B B
69 67 68 impel φ t A 𝑜 B t ran A CNF B y B A
70 fconstmpt B × = y B
71 69 70 fmptd φ t A 𝑜 B t ran A CNF B B × : B A
72 0ex V
73 72 a1i φ V
74 3 73 fczfsuppd φ finSupp B ×
75 74 adantr φ t A 𝑜 B t ran A CNF B finSupp B ×
76 1 2 3 cantnfs φ B × S B × : B A finSupp B ×
77 76 adantr φ t A 𝑜 B t ran A CNF B B × S B × : B A finSupp B ×
78 71 75 77 mpbir2and φ t A 𝑜 B t ran A CNF B B × S
79 eqid seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z = seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z
80 1 33 35 54 78 79 cantnfval φ t A 𝑜 B t ran A CNF B A CNF B B × = seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z dom OrdIso E
81 we0 E We
82 eqid OrdIso E = OrdIso E
83 82 oien V E We dom OrdIso E
84 72 81 83 mp2an dom OrdIso E
85 en0 dom OrdIso E dom OrdIso E =
86 84 85 mpbi dom OrdIso E =
87 86 fveq2i seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z dom OrdIso E = seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z
88 79 seqom0g V seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z =
89 72 88 ax-mp seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z =
90 87 89 eqtri seq ω k V , z V A 𝑜 OrdIso E k 𝑜 B × OrdIso E k + 𝑜 z dom OrdIso E =
91 80 90 eqtrdi φ t A 𝑜 B t ran A CNF B A CNF B B × =
92 14 adantr φ t A 𝑜 B t ran A CNF B A CNF B : S A 𝑜 B
93 92 ffnd φ t A 𝑜 B t ran A CNF B A CNF B Fn S
94 fnfvelrn A CNF B Fn S B × S A CNF B B × ran A CNF B
95 93 78 94 syl2anc φ t A 𝑜 B t ran A CNF B A CNF B B × ran A CNF B
96 91 95 eqeltrrd φ t A 𝑜 B t ran A CNF B ran A CNF B
97 32 50 96 pm2.61ne φ t A 𝑜 B t ran A CNF B t ran A CNF B
98 97 expr φ t A 𝑜 B t ran A CNF B t ran A CNF B
99 31 98 sylbid φ t A 𝑜 B y t y A 𝑜 B y ran A CNF B t ran A CNF B
100 99 ex φ t A 𝑜 B y t y A 𝑜 B y ran A CNF B t ran A CNF B
101 100 com23 φ y t y A 𝑜 B y ran A CNF B t A 𝑜 B t ran A CNF B
102 101 a2i φ y t y A 𝑜 B y ran A CNF B φ t A 𝑜 B t ran A CNF B
103 102 a1i t On φ y t y A 𝑜 B y ran A CNF B φ t A 𝑜 B t ran A CNF B
104 23 103 syl5bi t On y t φ y A 𝑜 B y ran A CNF B φ t A 𝑜 B t ran A CNF B
105 22 104 tfis2 t On φ t A 𝑜 B t ran A CNF B
106 105 com3l φ t A 𝑜 B t On t ran A CNF B
107 18 106 mpdd φ t A 𝑜 B t ran A CNF B
108 107 ssrdv φ A 𝑜 B ran A CNF B
109 15 108 eqssd φ ran A CNF B = A 𝑜 B
110 dffo2 A CNF B : S onto A 𝑜 B A CNF B : S A 𝑜 B ran A CNF B = A 𝑜 B
111 14 109 110 sylanbrc φ A CNF B : S onto A 𝑜 B
112 2 adantr φ f S g S f T g A On
113 3 adantr φ f S g S f T g B On
114 fveq2 z = t x z = x t
115 fveq2 z = t y z = y t
116 114 115 eleq12d z = t x z y z x t y t
117 eleq1w z = t z w t w
118 117 imbi1d z = t z w x w = y w t w x w = y w
119 118 ralbidv z = t w B z w x w = y w w B t w x w = y w
120 116 119 anbi12d z = t x z y z w B z w x w = y w x t y t w B t w x w = y w
121 120 cbvrexvw z B x z y z w B z w x w = y w t B x t y t w B t w x w = y w
122 fveq1 x = u x t = u t
123 fveq1 y = v y t = v t
124 eleq12 x t = u t y t = v t x t y t u t v t
125 122 123 124 syl2an x = u y = v x t y t u t v t
126 fveq1 x = u x w = u w
127 fveq1 y = v y w = v w
128 126 127 eqeqan12d x = u y = v x w = y w u w = v w
129 128 imbi2d x = u y = v t w x w = y w t w u w = v w
130 129 ralbidv x = u y = v w B t w x w = y w w B t w u w = v w
131 125 130 anbi12d x = u y = v x t y t w B t w x w = y w u t v t w B t w u w = v w
132 131 rexbidv x = u y = v t B x t y t w B t w x w = y w t B u t v t w B t w u w = v w
133 121 132 syl5bb x = u y = v z B x z y z w B z w x w = y w t B u t v t w B t w u w = v w
134 133 cbvopabv x y | z B x z y z w B z w x w = y w = u v | t B u t v t w B t w u w = v w
135 4 134 eqtri T = u v | t B u t v t w B t w u w = v w
136 simprll φ f S g S f T g f S
137 simprlr φ f S g S f T g g S
138 simprr φ f S g S f T g f T g
139 eqid c B | f c g c = c B | f c g c
140 eqid OrdIso E g supp = OrdIso E g supp
141 eqid seq ω k V , t V A 𝑜 OrdIso E g supp k 𝑜 g OrdIso E g supp k + 𝑜 t = seq ω k V , t V A 𝑜 OrdIso E g supp k 𝑜 g OrdIso E g supp k + 𝑜 t
142 1 112 113 135 136 137 138 139 140 141 cantnflem1 φ f S g S f T g A CNF B f A CNF B g
143 fvex A CNF B g V
144 143 epeli A CNF B f E A CNF B g A CNF B f A CNF B g
145 142 144 sylibr φ f S g S f T g A CNF B f E A CNF B g
146 145 expr φ f S g S f T g A CNF B f E A CNF B g
147 146 ralrimivva φ f S g S f T g A CNF B f E A CNF B g
148 soisoi T Or S E Po A 𝑜 B A CNF B : S onto A 𝑜 B f S g S f T g A CNF B f E A CNF B g A CNF B Isom T , E S A 𝑜 B
149 5 13 111 147 148 syl22anc φ A CNF B Isom T , E S A 𝑜 B