Theorem infxpenlem 8412

Description: Lemma for infxpen 8413. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)

Hypotheses

Ref	Expression
leweon.1
r0weon.1
infxpen.1
infxpen.2
infxpen.3
infxpen.4

Assertion

Ref	Expression
infxpenlem

Distinct variable groups:   ,   ,J   ,,   ,,M   ,,   ,Q   ,,,,,

Proof of Theorem infxpenlem

Step	Hyp	Ref	Expression
1		sseq2 3525	. . . 4
2		xpeq12 5023	. . . . . 6
3	2	anidms 645	. . . . 5
4		id 22	. . . . 5
5	3, 4	breq12d 4465	. . . 4
6	1, 5	imbi12d 320	. . 3
7		sseq2 3525	. . . 4
8		xpeq12 5023	. . . . . 6
9	8	anidms 645	. . . . 5
10		id 22	. . . . 5
11	9, 10	breq12d 4465	. . . 4
12	7, 11	imbi12d 320	. . 3
13		infxpen.2	. . . . . . . 8
14		vex 3112	. . . . . . . . . . . . 13
15	14, 14	xpex 6604	. . . . . . . . . . . 12
16		simpll 753	. . . . . . . . . . . . . . . . . 18
17	13, 16	sylbi 195	. . . . . . . . . . . . . . . . 17
18		onss 6626	. . . . . . . . . . . . . . . . 17
19	17, 18	syl 16	. . . . . . . . . . . . . . . 16
20		xpss12 5113	. . . . . . . . . . . . . . . 16
21	19, 19, 20	syl2anc 661	. . . . . . . . . . . . . . 15
22		leweon.1	. . . . . . . . . . . . . . . . 17
23		r0weon.1	. . . . . . . . . . . . . . . . 17
24	22, 23	r0weon 8411	. . . . . . . . . . . . . . . 16
25	24	simpli 458	. . . . . . . . . . . . . . 15
26		wess 4871	. . . . . . . . . . . . . . 15
27	21, 25, 26	mpisyl 18	. . . . . . . . . . . . . 14
28		weinxp 5072	. . . . . . . . . . . . . 14
29	27, 28	sylib 196	. . . . . . . . . . . . 13
30		infxpen.1	. . . . . . . . . . . . . 14
31		weeq1 4872	. . . . . . . . . . . . . 14
32	30, 31	ax-mp 5	. . . . . . . . . . . . 13
33	29, 32	sylibr 212	. . . . . . . . . . . 12
34		infxpen.4	. . . . . . . . . . . . 13
35	34	oiiso 7983	. . . . . . . . . . . 12
36	15, 33, 35	sylancr 663	. . . . . . . . . . 11
37		isof1o 6221	. . . . . . . . . . 11
38		f1ocnv 5833	. . . . . . . . . . 11
39		f1of1 5820	. . . . . . . . . . 11
40	36, 37, 38, 39	4syl 21	. . . . . . . . . 10
41		f1f1orn 5832	. . . . . . . . . 10
42	15	f1oen 7556	. . . . . . . . . 10
43	40, 41, 42	3syl 20	. . . . . . . . 9
44		f1ofn 5822	. . . . . . . . . . 11
45	36, 37, 38, 44	4syl 21	. . . . . . . . . 10
46	36	adantr 465	. . . . . . . . . . . . . . . . 17
47	37, 38, 39	3syl 20	. . . . . . . . . . . . . . . . . 18
48		cnvimass 5362	. . . . . . . . . . . . . . . . . . 19
49		inss2 3718	. . . . . . . . . . . . . . . . . . . . . 22
50	30, 49	eqsstri 3533	. . . . . . . . . . . . . . . . . . . . 21
51		dmss 5207	. . . . . . . . . . . . . . . . . . . . 21
52	50, 51	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
53		dmxpid 5227	. . . . . . . . . . . . . . . . . . . 20
54	52, 53	sseqtri 3535	. . . . . . . . . . . . . . . . . . 19
55	48, 54	sstri 3512	. . . . . . . . . . . . . . . . . 18
56		f1ores 5835	. . . . . . . . . . . . . . . . . 18
57	47, 55, 56	sylancl 662	. . . . . . . . . . . . . . . . 17
58	15, 15	xpex 6604	. . . . . . . . . . . . . . . . . . . . . 22
59	58	inex2 4594	. . . . . . . . . . . . . . . . . . . . 21
60	30, 59	eqeltri 2541	. . . . . . . . . . . . . . . . . . . 20
61	60	cnvex 6747	. . . . . . . . . . . . . . . . . . 19
62		imaexg 6737	. . . . . . . . . . . . . . . . . . 19
63	61, 62	ax-mp 5	. . . . . . . . . . . . . . . . . 18
64	63	f1oen 7556	. . . . . . . . . . . . . . . . 17
65	46, 57, 64	3syl 20	. . . . . . . . . . . . . . . 16
66		sseqin2 3716	. . . . . . . . . . . . . . . . . . 19
67	55, 66	mpbi 208	. . . . . . . . . . . . . . . . . 18
68	67	imaeq2i 5340	. . . . . . . . . . . . . . . . 17
69		isocnv 6226	. . . . . . . . . . . . . . . . . . . 20
70	46, 69	syl 16	. . . . . . . . . . . . . . . . . . 19
71		simpr 461	. . . . . . . . . . . . . . . . . . 19
72		isoini 6234	. . . . . . . . . . . . . . . . . . 19
73	70, 71, 72	syl2anc 661	. . . . . . . . . . . . . . . . . 18
74		fvex 5881	. . . . . . . . . . . . . . . . . . . . 21
75	74	epini 5372	. . . . . . . . . . . . . . . . . . . 20
76	75	ineq2i 3696	. . . . . . . . . . . . . . . . . . 19
77	34	oicl 7975	. . . . . . . . . . . . . . . . . . . . 21
78		f1of 5821	. . . . . . . . . . . . . . . . . . . . . . 23
79	36, 37, 38, 78	4syl 21	. . . . . . . . . . . . . . . . . . . . . 22
80	79	ffvelrnda 6031	. . . . . . . . . . . . . . . . . . . . 21
81		ordelss 4899	. . . . . . . . . . . . . . . . . . . . 21
82	77, 80, 81	sylancr 663	. . . . . . . . . . . . . . . . . . . 20
83		dfss1 3702	. . . . . . . . . . . . . . . . . . . 20
84	82, 83	sylib 196	. . . . . . . . . . . . . . . . . . 19
85	76, 84	syl5eq 2510	. . . . . . . . . . . . . . . . . 18
86	73, 85	eqtrd 2498	. . . . . . . . . . . . . . . . 17
87	68, 86	syl5eqr 2512	. . . . . . . . . . . . . . . 16
88	65, 87	breqtrd 4476	. . . . . . . . . . . . . . 15
89	88	ensymd 7586	. . . . . . . . . . . . . 14
90		infxpen.3	. . . . . . . . . . . . . . . . . . 19
91		fvex 5881	. . . . . . . . . . . . . . . . . . . 20
92		fvex 5881	. . . . . . . . . . . . . . . . . . . 20
93	91, 92	unex 6598	. . . . . . . . . . . . . . . . . . 19
94	90, 93	eqeltri 2541	. . . . . . . . . . . . . . . . . 18
95	94	sucex 6646	. . . . . . . . . . . . . . . . 17
96	95, 95	xpex 6604	. . . . . . . . . . . . . . . 16
97		xpss 5114	. . . . . . . . . . . . . . . . . . . 20
98		simp3 998	. . . . . . . . . . . . . . . . . . . . . 22
99		vex 3112	. . . . . . . . . . . . . . . . . . . . . . 23
100		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . 24
101	100	eliniseg 5371	. . . . . . . . . . . . . . . . . . . . . . 23
102	99, 101	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
103	98, 102	sylib 196	. . . . . . . . . . . . . . . . . . . . 21
104	30	breqi 4458	. . . . . . . . . . . . . . . . . . . . . . 23
105		brin 4501	. . . . . . . . . . . . . . . . . . . . . . 23
106	104, 105	bitri 249	. . . . . . . . . . . . . . . . . . . . . 22
107	106	simprbi 464	. . . . . . . . . . . . . . . . . . . . 21
108		brxp 5035	. . . . . . . . . . . . . . . . . . . . . 22
109	108	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
110	103, 107, 109	3syl 20	. . . . . . . . . . . . . . . . . . . 20
111	97, 110	sseldi 3501	. . . . . . . . . . . . . . . . . . 19
112	17	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22
113	112	3adant3 1016	. . . . . . . . . . . . . . . . . . . . 21
114		xp1st 6830	. . . . . . . . . . . . . . . . . . . . . 22
115		onelon 4908	. . . . . . . . . . . . . . . . . . . . . 22
116	114, 115	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21
117	113, 110, 116	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
118		eloni 4893	. . . . . . . . . . . . . . . . . . . . . . . . . 26
119		elxp7 6833	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
120	119	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . . . 26
121		ordunel 6662	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
122	121	3expib 1199	. . . . . . . . . . . . . . . . . . . . . . . . . 26
123	118, 120, 122	syl2im 38	. . . . . . . . . . . . . . . . . . . . . . . . 25
124	112, 71, 123	sylc 60	. . . . . . . . . . . . . . . . . . . . . . . 24
125	90, 124	syl5eqel 2549	. . . . . . . . . . . . . . . . . . . . . . 23
126		simprr 757	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
127	13, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
128		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
129	13, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26
130		iscard 8377	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
131		cardlim 8374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
132		sseq2 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
133		limeq 4895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
134	132, 133	bibi12d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
135	131, 134	mpbii 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
136	130, 135	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
137	136	biimpa 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26
138	17, 127, 129, 137	syl21anc 1227	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24
140		limsuc 6684	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 140	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
142	125, 141	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22
143		onelon 4908	. . . . . . . . . . . . . . . . . . . . . 22
144	112, 142, 143	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21
145	144	3adant3 1016	. . . . . . . . . . . . . . . . . . . 20
146		ssun1 3666	. . . . . . . . . . . . . . . . . . . . 21
147	146	a1i 11	. . . . . . . . . . . . . . . . . . . 20
148	106	simplbi 460	. . . . . . . . . . . . . . . . . . . . 21
149		df-br 4453	. . . . . . . . . . . . . . . . . . . . . . . . . 26
150	23	eleq2i 2535	. . . . . . . . . . . . . . . . . . . . . . . . . 26
151		opabid 4759	. . . . . . . . . . . . . . . . . . . . . . . . . 26
152	149, 150, 151	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . 25
153	152	simprbi 464	. . . . . . . . . . . . . . . . . . . . . . . 24
154		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . 25
155	154	orim2i 518	. . . . . . . . . . . . . . . . . . . . . . . 24
156	153, 155	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23
157		fvex 5881	. . . . . . . . . . . . . . . . . . . . . . . . 25
158		fvex 5881	. . . . . . . . . . . . . . . . . . . . . . . . 25
159	157, 158	unex 6598	. . . . . . . . . . . . . . . . . . . . . . . 24
160	159	elsuc 4952	. . . . . . . . . . . . . . . . . . . . . . 23
161	156, 160	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22
162		suceq 4948	. . . . . . . . . . . . . . . . . . . . . . 23
163	90, 162	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
164	161, 163	syl6eleqr 2556	. . . . . . . . . . . . . . . . . . . . 21
165	103, 148, 164	3syl 20	. . . . . . . . . . . . . . . . . . . 20
166		ontr2 4930	. . . . . . . . . . . . . . . . . . . . 21
167	166	imp 429	. . . . . . . . . . . . . . . . . . . 20
168	117, 145, 147, 165, 167	syl22anc 1229	. . . . . . . . . . . . . . . . . . 19
169		xp2nd 6831	. . . . . . . . . . . . . . . . . . . . . 22
170		onelon 4908	. . . . . . . . . . . . . . . . . . . . . 22
171	169, 170	sylan2 474	. . . . . . . . . . . . . . . . . . . . 21
172	113, 110, 171	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
173		ssun2 3667	. . . . . . . . . . . . . . . . . . . . 21
174	173	a1i 11	. . . . . . . . . . . . . . . . . . . 20
175		ontr2 4930	. . . . . . . . . . . . . . . . . . . . 21
176	175	imp 429	. . . . . . . . . . . . . . . . . . . 20
177	172, 145, 174, 165, 176	syl22anc 1229	. . . . . . . . . . . . . . . . . . 19
178		elxp7 6833	. . . . . . . . . . . . . . . . . . . 20
179	178	biimpri 206	. . . . . . . . . . . . . . . . . . 19
180	111, 168, 177, 179	syl12anc 1226	. . . . . . . . . . . . . . . . . 18
181	180	3expia 1198	. . . . . . . . . . . . . . . . 17
182	181	ssrdv 3509	. . . . . . . . . . . . . . . 16
183		ssdomg 7581	. . . . . . . . . . . . . . . 16
184	96, 182, 183	mpsyl 63	. . . . . . . . . . . . . . 15
185	129	adantr 465	. . . . . . . . . . . . . . . . 17
186		nnfi 7730	. . . . . . . . . . . . . . . . . . . 20
187		xpfi 7811	. . . . . . . . . . . . . . . . . . . . . 22
188	187	anidms 645	. . . . . . . . . . . . . . . . . . . . 21
189		isfinite 8090	. . . . . . . . . . . . . . . . . . . . 21
190	188, 189	sylib 196	. . . . . . . . . . . . . . . . . . . 20
191	186, 190	syl 16	. . . . . . . . . . . . . . . . . . 19
192		ssdomg 7581	. . . . . . . . . . . . . . . . . . . 20
193	14, 192	ax-mp 5	. . . . . . . . . . . . . . . . . . 19
194		sdomdomtr 7670	. . . . . . . . . . . . . . . . . . 19
195	191, 193, 194	syl2an 477	. . . . . . . . . . . . . . . . . 18
196	195	expcom 435	. . . . . . . . . . . . . . . . 17
197	185, 196	syl 16	. . . . . . . . . . . . . . . 16
198	127	adantr 465	. . . . . . . . . . . . . . . . . 18
199		breq1 4455	. . . . . . . . . . . . . . . . . . 19
200	199	rspccv 3207	. . . . . . . . . . . . . . . . . 18
201	198, 142, 200	sylc 60	. . . . . . . . . . . . . . . . 17
202		omelon 8084	. . . . . . . . . . . . . . . . . . 19
203		ontri1 4917	. . . . . . . . . . . . . . . . . . 19
204	202, 144, 203	sylancr 663	. . . . . . . . . . . . . . . . . 18
205		simplr 755	. . . . . . . . . . . . . . . . . . . . 21
206	13, 205	sylbi 195	. . . . . . . . . . . . . . . . . . . 20
207	206	adantr 465	. . . . . . . . . . . . . . . . . . 19
208		sseq2 3525	. . . . . . . . . . . . . . . . . . . . 21
209		xpeq12 5023	. . . . . . . . . . . . . . . . . . . . . . 23
210	209	anidms 645	. . . . . . . . . . . . . . . . . . . . . 22
211		id 22	. . . . . . . . . . . . . . . . . . . . . 22
212	210, 211	breq12d 4465	. . . . . . . . . . . . . . . . . . . . 21
213	208, 212	imbi12d 320	. . . . . . . . . . . . . . . . . . . 20
214	213	rspccv 3207	. . . . . . . . . . . . . . . . . . 19
215	207, 142, 214	sylc 60	. . . . . . . . . . . . . . . . . 18
216	204, 215	sylbird 235	. . . . . . . . . . . . . . . . 17
217		ensdomtr 7673	. . . . . . . . . . . . . . . . . 18
218	217	expcom 435	. . . . . . . . . . . . . . . . 17
219	201, 216, 218	sylsyld 56	. . . . . . . . . . . . . . . 16
220	197, 219	pm2.61d 158	. . . . . . . . . . . . . . 15
221		domsdomtr 7672	. . . . . . . . . . . . . . 15
222	184, 220, 221	syl2anc 661	. . . . . . . . . . . . . 14
223		ensdomtr 7673	. . . . . . . . . . . . . 14
224	89, 222, 223	syl2anc 661	. . . . . . . . . . . . 13
225		ordelon 4907	. . . . . . . . . . . . . . 15
226	77, 80, 225	sylancr 663	. . . . . . . . . . . . . 14
227		onenon 8351	. . . . . . . . . . . . . . 15
228	112, 227	syl 16	. . . . . . . . . . . . . 14
229		cardsdomel 8376	. . . . . . . . . . . . . 14
230	226, 228, 229	syl2anc 661	. . . . . . . . . . . . 13
231	224, 230	mpbid 210	. . . . . . . . . . . 12
232		eleq2 2530	. . . . . . . . . . . . . 14
233	130, 232	sylbir 213	. . . . . . . . . . . . 13
234	112, 198, 233	syl2anc 661	. . . . . . . . . . . 12
235	231, 234	mpbid 210	. . . . . . . . . . 11
236	235	ralrimiva 2871	. . . . . . . . . 10
237		fnfvrnss 6059	. . . . . . . . . . 11
238		ssdomg 7581	. . . . . . . . . . 11
239	14, 237, 238	mpsyl 63	. . . . . . . . . 10
240	45, 236, 239	syl2anc 661	. . . . . . . . 9
241		endomtr 7593	. . . . . . . . 9
242	43, 240, 241	syl2anc 661	. . . . . . . 8
243	13, 242	sylbir 213	. . . . . . 7
244		df1o2 7161	. . . . . . . . . . . 12
245		1onn 7307	. . . . . . . . . . . 12
246	244, 245	eqeltrri 2542	. . . . . . . . . . 11
247		nnsdom 8091	. . . . . . . . . . 11
248		sdomdom 7563	. . . . . . . . . . 11
249	246, 247, 248	mp2b 10	. . . . . . . . . 10
250		domtr 7588	. . . . . . . . . 10
251	249, 193, 250	sylancr 663	. . . . . . . . 9
252		0ex 4582	. . . . . . . . . . . 12
253	14, 252	xpsnen 7621	. . . . . . . . . . 11
254	253	ensymi 7585	. . . . . . . . . 10
255	14	xpdom2 7632	. . . . . . . . . 10
256		endomtr 7593	. . . . . . . . . 10
257	254, 255, 256	sylancr 663	. . . . . . . . 9
258	251, 257	syl 16	. . . . . . . 8
259	258	ad2antrl 727	. . . . . . 7
260		sbth 7657	. . . . . . 7
261	243, 259, 260	syl2anc 661	. . . . . 6
262	261	expr 615	. . . . 5
263		simplr 755	. . . . . . . 8
264		simpll 753	. . . . . . . . 9
265		simprr 757	. . . . . . . . 9
266		rexnal 2905	. . . . . . . . . 10
267		onelss 4925	. . . . . . . . . . . . 13
268		ssdomg 7581	. . . . . . . . . . . . 13
269	267, 268	syld 44	. . . . . . . . . . . 12
270		bren2 7566	. . . . . . . . . . . . 13
271	270	simplbi2 625	. . . . . . . . . . . 12
272	269, 271	syl6 33	. . . . . . . . . . 11
273	272	reximdvai 2929	. . . . . . . . . 10
274	266, 273	syl5bir 218	. . . . . . . . 9
275	264, 265, 274	sylc 60	. . . . . . . 8
276		r19.29 2992	. . . . . . . 8
277	263, 275, 276	syl2anc 661	. . . . . . 7
278		simprl 756	. . . . . . . 8
279		onelon 4908	. . . . . . . . . . . . . . . . 17
280		ensym 7584	. . . . . . . . . . . . . . . . . 18
281		domentr 7594	. . . . . . . . . . . . . . . . . 18
282	193, 280, 281	syl2an 477	. . . . . . . . . . . . . . . . 17
283		domnsym 7663	. . . . . . . . . . . . . . . . . . 19
284		nnsdom 8091	. . . . . . . . . . . . . . . . . . 19
285	283, 284	nsyl 121	. . . . . . . . . . . . . . . . . 18
286		ontri1 4917	. . . . . . . . . . . . . . . . . . 19
287	202, 286	mpan 670	. . . . . . . . . . . . . . . . . 18
288	285, 287	syl5ibr 221	. . . . . . . . . . . . . . . . 17
289	279, 282, 288	syl2im 38	. . . . . . . . . . . . . . . 16
290	289	expd 436	. . . . . . . . . . . . . . 15
291	290	impcom 430	. . . . . . . . . . . . . 14
292	291	imim1d 75	. . . . . . . . . . . . 13
293	292	imp32 433	. . . . . . . . . . . 12
294		entr 7587	. . . . . . . . . . . . . . . 16
295	294	ancoms 453	. . . . . . . . . . . . . . 15
296		xpen 7700	. . . . . . . . . . . . . . . . . 18
297	296	anidms 645	. . . . . . . . . . . . . . . . 17
298		entr 7587	. . . . . . . . . . . . . . . . 17
299	297, 298	sylan 471	. . . . . . . . . . . . . . . 16
300	280, 299	sylan 471	. . . . . . . . . . . . . . 15
301	295, 300	syldan 470	. . . . . . . . . . . . . 14
302	301	ex 434	. . . . . . . . . . . . 13
303	302	ad2antll 728	. . . . . . . . . . . 12
304	293, 303	mpd 15	. . . . . . . . . . 11
305	304	ex 434	. . . . . . . . . 10
306	305	expr 615	. . . . . . . . 9
307	306	rexlimdv 2947	. . . . . . . 8
308	278, 264, 307	syl2anc 661	. . . . . . 7
309	277, 308	mpd 15	. . . . . 6
310	309	expr 615	. . . . 5
311	262, 310	pm2.61d 158	. . . 4
312	311	exp31 604	. . 3
313	6, 12, 312	tfis3 6692	. 2
314	313	imp 429	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  \/wo 368  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  cvv 3109  u.cun 3473  i^icin 3474  C_wss 3475  c0 3784  {csn 4029  <.cop 4035   class class class wbr 4452  {copab 4509  cep 4794  Sewse 4841  Wewwe 4842  Ordword 4882  con0 4883  Limwlim 4884  succsuc 4885  X.cxp 5002  `'ccnv 5003  domcdm 5004  rancrn 5005  |`cres 5006  "cima 5007  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592  `cfv 5593  Isomwiso 5594  com 6700  c1st 6798  c2nd 6799  c1o 7142  cen 7533  cdom 7534  csdm 7535  cfn 7536  OrdIsocoi 7955  ccrd 8337

This theorem is referenced by:  infxpen  8413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-inf2 8079

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-se 4844  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-1o 7149  df-oadd 7153  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-oi 7956  df-card 8341