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.

Step	Hyp	Ref	Expression
1		cnfcomOLD.1	. 2
2		cnfcomOLD.s	. . . . . 6
3		omelon 8084	. . . . . . 7
4	3	a1i 11	. . . . . 6
5		cnfcomOLD.a	. . . . . 6
6		cnfcomOLD.g	. . . . . 6
7		cnfcomOLD.f	. . . . . . 7
8	2, 4, 5	cantnff1o 8158	. . . . . . . . 9
9		f1ocnv 5833	. . . . . . . . 9
10		f1of 5821	. . . . . . . . 9
11	8, 9, 10	3syl 20	. . . . . . . 8
12		cnfcomOLD.b	. . . . . . . 8
13	11, 12	ffvelrnd 6032	. . . . . . 7
14	7, 13	syl5eqel 2549	. . . . . 6
15	2, 4, 5, 6, 14	cantnfclOLD 8137	. . . . 5
16	15	simprd 463	. . . 4
17		elnn 6710	. . . 4
18	1, 16, 17	syl2anc 661	. . 3
19		eleq1 2529	. . . . . 6
20		suceq 4948	. . . . . . . 8
21	20	fveq2d 5875	. . . . . . 7
22	20	fveq2d 5875	. . . . . . 7
23		fveq2 5871	. . . . . . . . 9
24	23	oveq2d 6312	. . . . . . . 8
25	23	fveq2d 5875	. . . . . . . 8
26	24, 25	oveq12d 6314	. . . . . . 7
27	21, 22, 26	f1oeq123d 5818	. . . . . 6
28	19, 27	imbi12d 320	. . . . 5
29	28	imbi2d 316	. . . 4
30		eleq1 2529	. . . . . 6
31		suceq 4948	. . . . . . . 8
32	31	fveq2d 5875	. . . . . . 7
33	31	fveq2d 5875	. . . . . . 7
34		fveq2 5871	. . . . . . . . 9
35	34	oveq2d 6312	. . . . . . . 8
36	34	fveq2d 5875	. . . . . . . 8
37	35, 36	oveq12d 6314	. . . . . . 7
38	32, 33, 37	f1oeq123d 5818	. . . . . 6
39	30, 38	imbi12d 320	. . . . 5
40		eleq1 2529	. . . . . 6
41		suceq 4948	. . . . . . . 8
42	41	fveq2d 5875	. . . . . . 7
43	41	fveq2d 5875	. . . . . . 7
44		fveq2 5871	. . . . . . . . 9
45	44	oveq2d 6312	. . . . . . . 8
46	44	fveq2d 5875	. . . . . . . 8
47	45, 46	oveq12d 6314	. . . . . . 7
48	42, 43, 47	f1oeq123d 5818	. . . . . 6
49	40, 48	imbi12d 320	. . . . 5
50		eleq1 2529	. . . . . 6
51		suceq 4948	. . . . . . . 8
52	51	fveq2d 5875	. . . . . . 7
53	51	fveq2d 5875	. . . . . . 7
54		fveq2 5871	. . . . . . . . 9
55	54	oveq2d 6312	. . . . . . . 8
56	54	fveq2d 5875	. . . . . . . 8
57	55, 56	oveq12d 6314	. . . . . . 7
58	52, 53, 57	f1oeq123d 5818	. . . . . 6
59	50, 58	imbi12d 320	. . . . 5
60	5	adantr 465	. . . . . . 7
61	12	adantr 465	. . . . . . 7
62		cnfcomOLD.h	. . . . . . 7
63		cnfcomOLD.t	. . . . . . 7
64		cnfcomOLD.m	. . . . . . 7
65		cnfcomOLD.k	. . . . . . 7
66		simpr 461	. . . . . . 7
67	3	a1i 11	. . . . . . . 8
68		cnvimass 5362	. . . . . . . . . . 11
69	2, 4, 5	cantnfsOLD 8136	. . . . . . . . . . . . . 14
70	14, 69	mpbid 210	. . . . . . . . . . . . 13
71	70	simpld 459	. . . . . . . . . . . 12
72		fdm 5740	. . . . . . . . . . . 12
73	71, 72	syl 16	. . . . . . . . . . 11
74	68, 73	syl5sseq 3551	. . . . . . . . . 10
75		onss 6626	. . . . . . . . . . 11
76	5, 75	syl 16	. . . . . . . . . 10
77	74, 76	sstrd 3513	. . . . . . . . 9
78	6	oif 7976	. . . . . . . . . 10
79	78	ffvelrni 6030	. . . . . . . . 9
80		ssel2 3498	. . . . . . . . 9
81	77, 79, 80	syl2an 477	. . . . . . . 8
82		peano1 6719	. . . . . . . . 9
83	82	a1i 11	. . . . . . . 8
84		oen0 7254	. . . . . . . 8
85	67, 81, 83, 84	syl21anc 1227	. . . . . . 7
86		0ex 4582	. . . . . . . . 9
87	63	seqom0g 7140	. . . . . . . . 9
88	86, 87	ax-mp 5	. . . . . . . 8
89		f1o0 5855	. . . . . . . . . 10
90	62	seqom0g 7140	. . . . . . . . . . 11
91		f1oeq2 5813	. . . . . . . . . . 11
92	86, 90, 91	mp2b 10	. . . . . . . . . 10
93	89, 92	mpbir 209	. . . . . . . . 9
94		f1oeq1 5812	. . . . . . . . 9
95	93, 94	mpbiri 233	. . . . . . . 8
96	88, 95	mp1i 12	. . . . . . 7
97	2, 60, 61, 7, 6, 62, 63, 64, 65, 66, 85, 96	cnfcomlemOLD 8172	. . . . . 6
98	97	ex 434	. . . . 5
99	6	oicl 7975	. . . . . . . . . 10
100		ordtr 4897	. . . . . . . . . 10
101	99, 100	ax-mp 5	. . . . . . . . 9
102		trsuc 4967	. . . . . . . . 9
103	101, 102	mpan 670	. . . . . . . 8
104	103	imim1i 58	. . . . . . 7
105	5	ad2antrr 725	. . . . . . . . . 10
106	12	ad2antrr 725	. . . . . . . . . 10
107		simprl 756	. . . . . . . . . 10
108	76	ad2antrr 725	. . . . . . . . . . . . . . 15
109	74	ad2antrr 725	. . . . . . . . . . . . . . . 16
110	78	ffvelrni 6030	. . . . . . . . . . . . . . . . 17
111	110	ad2antrl 727	. . . . . . . . . . . . . . . 16
112	109, 111	sseldd 3504	. . . . . . . . . . . . . . 15
113	108, 112	sseldd 3504	. . . . . . . . . . . . . 14
114		eloni 4893	. . . . . . . . . . . . . 14
115	113, 114	syl 16	. . . . . . . . . . . . 13
116		vex 3112	. . . . . . . . . . . . . . 15
117	116	sucid 4962	. . . . . . . . . . . . . 14
118	5, 74	ssexd 4599	. . . . . . . . . . . . . . . . . 18
119	15	simpld 459	. . . . . . . . . . . . . . . . . 18
120	6	oiiso 7983	. . . . . . . . . . . . . . . . . 18
121	118, 119, 120	syl2anc 661	. . . . . . . . . . . . . . . . 17
122	121	ad2antrr 725	. . . . . . . . . . . . . . . 16
123	103	ad2antrl 727	. . . . . . . . . . . . . . . 16
124		isorel 6222	. . . . . . . . . . . . . . . 16
125	122, 123, 107, 124	syl12anc 1226	. . . . . . . . . . . . . . 15
126	116	sucex 6646	. . . . . . . . . . . . . . . 16
127	126	epelc 4798	. . . . . . . . . . . . . . 15
128		fvex 5881	. . . . . . . . . . . . . . . 16
129	128	epelc 4798	. . . . . . . . . . . . . . 15
130	125, 127, 129	3bitr3g 287	. . . . . . . . . . . . . 14
131	117, 130	mpbii 211	. . . . . . . . . . . . 13
132		ordsucss 6653	. . . . . . . . . . . . 13
133	115, 131, 132	sylc 60	. . . . . . . . . . . 12
134	78	ffvelrni 6030	. . . . . . . . . . . . . . . . 17
135	123, 134	syl 16	. . . . . . . . . . . . . . . 16
136	109, 135	sseldd 3504	. . . . . . . . . . . . . . 15
137	108, 136	sseldd 3504	. . . . . . . . . . . . . 14
138		suceloni 6648	. . . . . . . . . . . . . 14
139	137, 138	syl 16	. . . . . . . . . . . . 13
140	3	a1i 11	. . . . . . . . . . . . 13
141	82	a1i 11	. . . . . . . . . . . . 13
142		oewordi 7259	. . . . . . . . . . . . 13
143	139, 113, 140, 141, 142	syl31anc 1231	. . . . . . . . . . . 12
144	133, 143	mpd 15	. . . . . . . . . . 11
145	71	ad2antrr 725	. . . . . . . . . . . . . 14
146	145, 136	ffvelrnd 6032	. . . . . . . . . . . . 13
147		nnon 6706	. . . . . . . . . . . . . . 15
148	146, 147	syl 16	. . . . . . . . . . . . . 14
149		oecl 7206	. . . . . . . . . . . . . . 15
150	140, 137, 149	syl2anc 661	. . . . . . . . . . . . . 14
151		oen0 7254	. . . . . . . . . . . . . . 15
152	140, 137, 141, 151	syl21anc 1227	. . . . . . . . . . . . . 14
153		omord2 7235	. . . . . . . . . . . . . 14
154	148, 140, 150, 152, 153	syl31anc 1231	. . . . . . . . . . . . 13
155	146, 154	mpbid 210	. . . . . . . . . . . 12
156		oesuc 7196	. . . . . . . . . . . . 13
157	140, 137, 156	syl2anc 661	. . . . . . . . . . . 12
158	155, 157	eleqtrrd 2548	. . . . . . . . . . 11
159	144, 158	sseldd 3504	. . . . . . . . . 10
160		simprr 757	. . . . . . . . . 10
161	2, 105, 106, 7, 6, 62, 63, 64, 65, 107, 159, 160	cnfcomlemOLD 8172	. . . . . . . . 9
162	161	exp32 605	. . . . . . . 8
163	162	a2d 26	. . . . . . 7
164	104, 163	syl5 32	. . . . . 6
165	164	expcom 435	. . . . 5