MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnfcomOLD Unicode version

Theorem cnfcomOLD 8173
Description: Any ordinal is equinumerous to the leading term of its Cantor normal form. Here we show that bijection explicitly. (Contributed by Mario Carneiro, 30-May-2015.) Obsolete version of cnfcom 8165 as of 3-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cnfcomOLD.s
cnfcomOLD.a
cnfcomOLD.b
cnfcomOLD.f
cnfcomOLD.g
cnfcomOLD.h
cnfcomOLD.t
cnfcomOLD.m
cnfcomOLD.k
cnfcomOLD.1
Assertion
Ref Expression
cnfcomOLD
Distinct variable groups:   , , ,   ,I, ,   ,M   , , , ,   ,   , , , ,   , ,   S, ,

Proof of Theorem cnfcomOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnfcomOLD.1 . 2
2 cnfcomOLD.s . . . . . 6
3 omelon 8084 . . . . . . 7
43a1i 11 . . . . . 6
5 cnfcomOLD.a . . . . . 6
6 cnfcomOLD.g . . . . . 6
7 cnfcomOLD.f . . . . . . 7
82, 4, 5cantnff1o 8158 . . . . . . . . 9
9 f1ocnv 5833 . . . . . . . . 9
10 f1of 5821 . . . . . . . . 9
118, 9, 103syl 20 . . . . . . . 8
12 cnfcomOLD.b . . . . . . . 8
1311, 12ffvelrnd 6032 . . . . . . 7
147, 13syl5eqel 2549 . . . . . 6
152, 4, 5, 6, 14cantnfclOLD 8137 . . . . 5
1615simprd 463 . . . 4
17 elnn 6710 . . . 4
181, 16, 17syl2anc 661 . . 3
19 eleq1 2529 . . . . . 6
20 suceq 4948 . . . . . . . 8
2120fveq2d 5875 . . . . . . 7
2220fveq2d 5875 . . . . . . 7
23 fveq2 5871 . . . . . . . . 9
2423oveq2d 6312 . . . . . . . 8
2523fveq2d 5875 . . . . . . . 8
2624, 25oveq12d 6314 . . . . . . 7
2721, 22, 26f1oeq123d 5818 . . . . . 6
2819, 27imbi12d 320 . . . . 5
2928imbi2d 316 . . . 4
30 eleq1 2529 . . . . . 6
31 suceq 4948 . . . . . . . 8
3231fveq2d 5875 . . . . . . 7
3331fveq2d 5875 . . . . . . 7
34 fveq2 5871 . . . . . . . . 9
3534oveq2d 6312 . . . . . . . 8
3634fveq2d 5875 . . . . . . . 8
3735, 36oveq12d 6314 . . . . . . 7
3832, 33, 37f1oeq123d 5818 . . . . . 6
3930, 38imbi12d 320 . . . . 5
40 eleq1 2529 . . . . . 6
41 suceq 4948 . . . . . . . 8
4241fveq2d 5875 . . . . . . 7
4341fveq2d 5875 . . . . . . 7
44 fveq2 5871 . . . . . . . . 9
4544oveq2d 6312 . . . . . . . 8
4644fveq2d 5875 . . . . . . . 8
4745, 46oveq12d 6314 . . . . . . 7
4842, 43, 47f1oeq123d 5818 . . . . . 6
4940, 48imbi12d 320 . . . . 5
50 eleq1 2529 . . . . . 6
51 suceq 4948 . . . . . . . 8
5251fveq2d 5875 . . . . . . 7
5351fveq2d 5875 . . . . . . 7
54 fveq2 5871 . . . . . . . . 9
5554oveq2d 6312 . . . . . . . 8
5654fveq2d 5875 . . . . . . . 8
5755, 56oveq12d 6314 . . . . . . 7
5852, 53, 57f1oeq123d 5818 . . . . . 6
5950, 58imbi12d 320 . . . . 5
605adantr 465 . . . . . . 7
6112adantr 465 . . . . . . 7
62 cnfcomOLD.h . . . . . . 7
63 cnfcomOLD.t . . . . . . 7
64 cnfcomOLD.m . . . . . . 7
65 cnfcomOLD.k . . . . . . 7
66 simpr 461 . . . . . . 7
673a1i 11 . . . . . . . 8
68 cnvimass 5362 . . . . . . . . . . 11
692, 4, 5cantnfsOLD 8136 . . . . . . . . . . . . . 14
7014, 69mpbid 210 . . . . . . . . . . . . 13
7170simpld 459 . . . . . . . . . . . 12
72 fdm 5740 . . . . . . . . . . . 12
7371, 72syl 16 . . . . . . . . . . 11
7468, 73syl5sseq 3551 . . . . . . . . . 10
75 onss 6626 . . . . . . . . . . 11
765, 75syl 16 . . . . . . . . . 10
7774, 76sstrd 3513 . . . . . . . . 9
786oif 7976 . . . . . . . . . 10
7978ffvelrni 6030 . . . . . . . . 9
80 ssel2 3498 . . . . . . . . 9
8177, 79, 80syl2an 477 . . . . . . . 8
82 peano1 6719 . . . . . . . . 9
8382a1i 11 . . . . . . . 8
84 oen0 7254 . . . . . . . 8
8567, 81, 83, 84syl21anc 1227 . . . . . . 7
86 0ex 4582 . . . . . . . . 9
8763seqom0g 7140 . . . . . . . . 9
8886, 87ax-mp 5 . . . . . . . 8
89 f1o0 5855 . . . . . . . . . 10
9062seqom0g 7140 . . . . . . . . . . 11
91 f1oeq2 5813 . . . . . . . . . . 11
9286, 90, 91mp2b 10 . . . . . . . . . 10
9389, 92mpbir 209 . . . . . . . . 9
94 f1oeq1 5812 . . . . . . . . 9
9593, 94mpbiri 233 . . . . . . . 8
9688, 95mp1i 12 . . . . . . 7
972, 60, 61, 7, 6, 62, 63, 64, 65, 66, 85, 96cnfcomlemOLD 8172 . . . . . 6
9897ex 434 . . . . 5
996oicl 7975 . . . . . . . . . 10
100 ordtr 4897 . . . . . . . . . 10
10199, 100ax-mp 5 . . . . . . . . 9
102 trsuc 4967 . . . . . . . . 9
103101, 102mpan 670 . . . . . . . 8
104103imim1i 58 . . . . . . 7
1055ad2antrr 725 . . . . . . . . . 10
10612ad2antrr 725 . . . . . . . . . 10
107 simprl 756 . . . . . . . . . 10
10876ad2antrr 725 . . . . . . . . . . . . . . 15
10974ad2antrr 725 . . . . . . . . . . . . . . . 16
11078ffvelrni 6030 . . . . . . . . . . . . . . . . 17
111110ad2antrl 727 . . . . . . . . . . . . . . . 16
112109, 111sseldd 3504 . . . . . . . . . . . . . . 15
113108, 112sseldd 3504 . . . . . . . . . . . . . 14
114 eloni 4893 . . . . . . . . . . . . . 14
115113, 114syl 16 . . . . . . . . . . . . 13
116 vex 3112 . . . . . . . . . . . . . . 15
117116sucid 4962 . . . . . . . . . . . . . 14
1185, 74ssexd 4599 . . . . . . . . . . . . . . . . . 18
11915simpld 459 . . . . . . . . . . . . . . . . . 18
1206oiiso 7983 . . . . . . . . . . . . . . . . . 18
121118, 119, 120syl2anc 661 . . . . . . . . . . . . . . . . 17
122121ad2antrr 725 . . . . . . . . . . . . . . . 16
123103ad2antrl 727 . . . . . . . . . . . . . . . 16
124 isorel 6222 . . . . . . . . . . . . . . . 16
125122, 123, 107, 124syl12anc 1226 . . . . . . . . . . . . . . 15
126116sucex 6646 . . . . . . . . . . . . . . . 16
127126epelc 4798 . . . . . . . . . . . . . . 15
128 fvex 5881 . . . . . . . . . . . . . . . 16
129128epelc 4798 . . . . . . . . . . . . . . 15
130125, 127, 1293bitr3g 287 . . . . . . . . . . . . . 14
131117, 130mpbii 211 . . . . . . . . . . . . 13
132 ordsucss 6653 . . . . . . . . . . . . 13
133115, 131, 132sylc 60 . . . . . . . . . . . 12
13478ffvelrni 6030 . . . . . . . . . . . . . . . . 17
135123, 134syl 16 . . . . . . . . . . . . . . . 16
136109, 135sseldd 3504 . . . . . . . . . . . . . . 15
137108, 136sseldd 3504 . . . . . . . . . . . . . 14
138 suceloni 6648 . . . . . . . . . . . . . 14
139137, 138syl 16 . . . . . . . . . . . . 13
1403a1i 11 . . . . . . . . . . . . 13
14182a1i 11 . . . . . . . . . . . . 13
142 oewordi 7259 . . . . . . . . . . . . 13
143139, 113, 140, 141, 142syl31anc 1231 . . . . . . . . . . . 12
144133, 143mpd 15 . . . . . . . . . . 11
14571ad2antrr 725 . . . . . . . . . . . . . 14
146145, 136ffvelrnd 6032 . . . . . . . . . . . . 13
147 nnon 6706 . . . . . . . . . . . . . . 15
148146, 147syl 16 . . . . . . . . . . . . . 14
149 oecl 7206 . . . . . . . . . . . . . . 15
150140, 137, 149syl2anc 661 . . . . . . . . . . . . . 14
151 oen0 7254 . . . . . . . . . . . . . . 15
152140, 137, 141, 151syl21anc 1227 . . . . . . . . . . . . . 14
153 omord2 7235 . . . . . . . . . . . . . 14
154148, 140, 150, 152, 153syl31anc 1231 . . . . . . . . . . . . 13
155146, 154mpbid 210 . . . . . . . . . . . 12
156 oesuc 7196 . . . . . . . . . . . . 13
157140, 137, 156syl2anc 661 . . . . . . . . . . . 12
158155, 157eleqtrrd 2548 . . . . . . . . . . 11
159144, 158sseldd 3504 . . . . . . . . . 10
160 simprr 757 . . . . . . . . . 10
1612, 105, 106, 7, 6, 62, 63, 64, 65, 107, 159, 160cnfcomlemOLD 8172 . . . . . . . . 9
162161exp32 605 . . . . . . . 8
163162a2d 26 . . . . . . 7
164104, 163syl5 32 . . . . . 6
165164expcom 435 . . . . 5