cmpfi - Metamath Proof Explorer

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

Theorem cmpfi 20435

Description: If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)

**Assertion**
Ref	Expression
cmpfi

Distinct variable group:

Proof of Theorem cmpfi Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elpwi 3962	. . . 4
2		0ss 3765	. . . . . . . . . . 11
3		0fin 7804	. . . . . . . . . . 11
4		elfpw 7881	. . . . . . . . . . 11 $/\$
5	2, 3, 4	mpbir2an 932	. . . . . . . . . 10
6		simprr 767	. . . . . . . . . . 11 $/\$ $/\$ $/\$
7		simprl 765	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
8	7	unieqd 4211	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	6, 8	eqtrd 2487	. . . . . . . . . 10 $/\$ $/\$ $/\$
10		unieq 4209	. . . . . . . . . . . 12
11	10	eqeq2d 2463	. . . . . . . . . . 11
12	11	rspcev 3152	. . . . . . . . . 10 $/\$
13	5, 9, 12	sylancr 670	. . . . . . . . 9 $/\$ $/\$ $/\$
14	13	expr 620	. . . . . . . 8 $/\$ $/\$
15		vn0 3741	. . . . . . . . . 10
16		iineq1 4296	. . . . . . . . . . . . . 14 $\$ $\$
17	16	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
18		0iin 4339	. . . . . . . . . . . . 13 $\$
19	17, 18	syl6eq 2503	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20	19	eqeq1d 2455	. . . . . . . . . . 11 $/\$ $/\$ $\$
21	20	necon3bbid 2663	. . . . . . . . . 10 $/\$ $/\$ $\$
22	15, 21	mpbiri 237	. . . . . . . . 9 $/\$ $/\$ $\$
23	22	pm2.21d 110	. . . . . . . 8 $/\$ $/\$ $\$ $\$
24	14, 23	2thd 244	. . . . . . 7 $/\$ $/\$ $\$ $\$
25		uniss 4222	. . . . . . . . . . . 12
26	25	ad2antlr 734	. . . . . . . . . . 11 $/\$ $/\$
27		eqss 3449	. . . . . . . . . . . 12 $/\$
28	27	baib 915	. . . . . . . . . . 11
29	26, 28	syl 17	. . . . . . . . . 10 $/\$ $/\$
30		eqcom 2460	. . . . . . . . . 10
31		ssdif0 3825	. . . . . . . . . 10 $\$
32	29, 30, 31	3bitr3g 291	. . . . . . . . 9 $/\$ $/\$ $\$
33		iindif2 4350	. . . . . . . . . . . 12 $\$ $\$
34	33	adantl 468	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
35		uniiun 4334	. . . . . . . . . . . 12
36	35	difeq2i 3550	. . . . . . . . . . 11 $\$ $\$
37	34, 36	syl6eqr 2505	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
38	37	eqeq1d 2455	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
39	32, 38	bitr4d 260	. . . . . . . 8 $/\$ $/\$ $\$
40		imassrn 5182	. . . . . . . . . . . 12 $\$ $\$
41		df-ima 4850	. . . . . . . . . . . . . 14 $\$ $\$
42		resmpt 5157	. . . . . . . . . . . . . . . 16 $\$ $\$
43	42	adantl 468	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
44	43	rneqd 5065	. . . . . . . . . . . . . 14 $/\$ $\$ $\$
45	41, 44	syl5eq 2499	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46	45	ad2antrr 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
47	40, 46	syl5sseqr 3483	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
48		funmpt 5621	. . . . . . . . . . . 12 $\$
49		elfpw 7881	. . . . . . . . . . . . . 14 $/\$
50	49	simprbi 466	. . . . . . . . . . . . 13
51	50	adantl 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
52		imafi 7872	. . . . . . . . . . . 12 $\$ $/\$ $\$
53	48, 51, 52	sylancr 670	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
54		elfpw 7881	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $/\$ $\$
55	47, 53, 54	sylanbrc 671	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
56		eqid 2453	. . . . . . . . . . . . . . . . 17
57	56	topopn 19948	. . . . . . . . . . . . . . . 16
58		difexg 4554	. . . . . . . . . . . . . . . 16 $\$
59	57, 58	syl 17	. . . . . . . . . . . . . . 15 $\$
60	59	ralrimivw 2805	. . . . . . . . . . . . . 14 $\$
61		eqid 2453	. . . . . . . . . . . . . . 15 $\$ $\$
62	61	fnmpt 5709	. . . . . . . . . . . . . 14 $\$ $\$
63	60, 62	syl 17	. . . . . . . . . . . . 13 $\$
64	63	ad3antrrr 737	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
65		simpr 463	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$
66		elfpw 7881	. . . . . . . . . . . . . . 15 $\$ $\$ $/\$
67	65, 66	sylib 200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$ $/\$
68	67	simpld 461	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
69	45	ad2antrr 733	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$ $\$
70	68, 69	sseqtrd 3470	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
71	67	simprd 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
72		fipreima 7885	. . . . . . . . . . . 12 $\$ $/\$ $\$ $/\$ $\$
73	64, 70, 71, 72	syl3anc 1269	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
74		eqcom 2460	. . . . . . . . . . . 12 $\$ $\$
75	74	rexbii 2891	. . . . . . . . . . 11 $\$ $\$
76	73, 75	sylib 200	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
77		simpr 463	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
78	77	inteqd 4242	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
79	78	eqeq2d 2463	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
80	55, 76, 79	rexxfrd 4618	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
81		0ex 4538	. . . . . . . . . 10
82		imassrn 5182	. . . . . . . . . . . . 13 $\$ $\$
83		eqid 2453	. . . . . . . . . . . . . . . . 17 $\$ $\$
84	56, 83	opncldf1 20112	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$
85	84	simpld 461	. . . . . . . . . . . . . . 15 $\$
86		f1ofo 5826	. . . . . . . . . . . . . . 15 $\$ $\$
87	85, 86	syl 17	. . . . . . . . . . . . . 14 $\$
88		forn 5801	. . . . . . . . . . . . . 14 $\$ $\$
89	87, 88	syl 17	. . . . . . . . . . . . 13 $\$
90	82, 89	syl5sseq 3482	. . . . . . . . . . . 12 $\$
91		fvex 5880	. . . . . . . . . . . . 13
92	91	elpw2 4570	. . . . . . . . . . . 12 $\$ $\$
93	90, 92	sylibr 216	. . . . . . . . . . 11 $\$
94	93	ad2antrr 733	. . . . . . . . . 10 $/\$ $/\$ $\$
95		elfi 7932	. . . . . . . . . 10 $/\$ $\$ $\$ $\$
96	81, 94, 95	sylancr 670	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
97		inundif 3847	. . . . . . . . . . . . . 14 $\$
98	97	rexeqi 2994	. . . . . . . . . . . . 13 $\$
99		rexun 3616	. . . . . . . . . . . . 13 $\$ $\/$ $\$
100	98, 99	bitr3i 255	. . . . . . . . . . . 12 $\/$ $\$
101		inss2 3655	. . . . . . . . . . . . . . . . . . . . . 22
102	101	sseli 3430	. . . . . . . . . . . . . . . . . . . . 21
103		elsni 3995	. . . . . . . . . . . . . . . . . . . . 21
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . 20
105	104	unieqd 4211	. . . . . . . . . . . . . . . . . . 19
106		uni0 4228	. . . . . . . . . . . . . . . . . . 19
107	105, 106	syl6eq 2503	. . . . . . . . . . . . . . . . . 18
108	107	eqeq2d 2463	. . . . . . . . . . . . . . . . 17
109	108	biimpd 211	. . . . . . . . . . . . . . . 16
110	109	rexlimiv 2875	. . . . . . . . . . . . . . 15
111		ssid 3453	. . . . . . . . . . . . . . . . . . . 20
112	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
113		simprr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
114		0ss 3765	. . . . . . . . . . . . . . . . . . . . . . . . 25
115	113, 114	syl6eqss 3484	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
116	25	ad2antlr 734	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
117	115, 116	eqssd 3451	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
118	117, 113	eqtr3d 2489	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
119	118, 3	syl6eqel 2539	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
120		pwfi 7874	. . . . . . . . . . . . . . . . . . . . 21
121	119, 120	sylib 200	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
122		pwuni 4634	. . . . . . . . . . . . . . . . . . . 20
123		ssfi 7797	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	121, 122, 123	sylancl 669	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
125		elfpw 7881	. . . . . . . . . . . . . . . . . . 19 $/\$
126	112, 124, 125	sylanbrc 671	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
127		simprl 765	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
128		eldifsn 4100	. . . . . . . . . . . . . . . . . 18 $\$ $/\$
129	126, 127, 128	sylanbrc 671	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
130		unieq 4209	. . . . . . . . . . . . . . . . . . 19
131	130	eqeq2d 2463	. . . . . . . . . . . . . . . . . 18
132	131	rspcev 3152	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$
133	129, 117, 132	syl2anc 667	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
134	133	expr 620	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
135	110, 134	syl5 33	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
136		idd 25	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
137	135, 136	jaod 382	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $\$ $\$
138		olc 386	. . . . . . . . . . . . 13 $\$ $\/$ $\$
139	137, 138	impbid1 207	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $\$ $\$
140	100, 139	syl5bb 261	. . . . . . . . . . 11 $/\$ $/\$ $\$
141		eldifi 3557	. . . . . . . . . . . . . . . . . . . 20 $\$
142	141	adantl 468	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
143	142, 49	sylib 200	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$ $/\$
144	143	simpld 461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
145		simpllr 770	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
146	144, 145	sstrd 3444	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
147	146	unissd 4225	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
148		eqss 3449	. . . . . . . . . . . . . . . 16 $/\$
149	148	baib 915	. . . . . . . . . . . . . . 15
150	147, 149	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
151		eqcom 2460	. . . . . . . . . . . . . 14
152		ssdif0 3825	. . . . . . . . . . . . . . 15 $\$
153		eqcom 2460	. . . . . . . . . . . . . . 15 $\$ $\$
154	152, 153	bitri 253	. . . . . . . . . . . . . 14 $\$
155	150, 151, 154	3bitr3g 291	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
156		df-ima 4850	. . . . . . . . . . . . . . . . . 18 $\$ $\$
157	144	resmptd 5159	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$ $\$ $\$
158	157	rneqd 5065	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$ $\$ $\$
159	156, 158	syl5eq 2499	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $\$ $\$
160	159	inteqd 4242	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
161	59	ralrimivw 2805	. . . . . . . . . . . . . . . . . 18 $\$
162	161	ad3antrrr 737	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $\$
163		dfiin3g 5091	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
164	162, 163	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
165		eldifsn 4100	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
166	165	simprbi 466	. . . . . . . . . . . . . . . . . 18 $\$
167	166	adantl 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
168		iindif2 4350	. . . . . . . . . . . . . . . . 17 $\$ $\$
169	167, 168	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
170	160, 164, 169	3eqtr2d 2493	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$ $\$
171		uniiun 4334	. . . . . . . . . . . . . . . 16
172	171	difeq2i 3550	. . . . . . . . . . . . . . 15 $\$ $\$
173	170, 172	syl6eqr 2505	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$ $\$
174	173	eqeq2d 2463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$ $\$
175	155, 174	bitr4d 260	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
176	175	rexbidva 2900	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$ $\$
177	140, 176	bitrd 257	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
178		imaeq2 5167	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
179		ima0 5186	. . . . . . . . . . . . . . . . . . . 20 $\$
180	178, 179	syl6eq 2503	. . . . . . . . . . . . . . . . . . 19 $\$
181	180	inteqd 4242	. . . . . . . . . . . . . . . . . 18 $\$
182		int0 4251	. . . . . . . . . . . . . . . . . 18
183	181, 182	syl6eq 2503	. . . . . . . . . . . . . . . . 17 $\$
184	183	neeq1d 2685	. . . . . . . . . . . . . . . 16 $\$
185	15, 184	mpbiri 237	. . . . . . . . . . . . . . 15 $\$
186	185	necomd 2681	. . . . . . . . . . . . . 14 $\$
187	186	necon2i 2660	. . . . . . . . . . . . 13 $\$
188	165	rbaibr 917	. . . . . . . . . . . . 13 $\$
189	187, 188	syl 17	. . . . . . . . . . . 12 $\$ $\$
190	189	pm5.32ri 644	. . . . . . . . . . 11 $/\$ $\$ $\$ $/\$ $\$
191	190	rexbii2 2889	. . . . . . . . . 10 $\$ $\$ $\$
192	177, 191	syl6bbr 267	. . . . . . . . 9 $/\$ $/\$ $\$
193	80, 96, 192	3bitr4rd 290	. . . . . . . 8 $/\$ $/\$ $\$
194	39, 193	imbi12d 322	. . . . . . 7 $/\$ $/\$ $\$ $\$
195	24, 194	pm2.61dane 2713	. . . . . 6 $/\$ $\$ $\$
196	60	adantr 467	. . . . . . . . . . 11 $/\$ $\$
197		dfiin3g 5091	. . . . . . . . . . 11 $\$ $\$ $\$
198	196, 197	syl 17	. . . . . . . . . 10 $/\$ $\$ $\$
199	45	inteqd 4242	. . . . . . . . . 10 $/\$ $\$ $\$
200	198, 199	eqtr4d 2490	. . . . . . . . 9 $/\$ $\$ $\$
201	200	eqeq1d 2455	. . . . . . . 8 $/\$ $\$ $\$
202		nne 2630	. . . . . . . 8 $\$ $\$
203	201, 202	syl6bbr 267	. . . . . . 7 $/\$ $\$ $\$
204	203	imbi1d 319	. . . . . 6 $/\$ $\$ $\$ $\$ $\$
205	195, 204	bitrd 257	. . . . 5 $/\$ $\$ $\$
206		con1b 335	. . . . 5 $\$ $\$ $\$ $\$
207	205, 206	syl6bb 265	. . . 4 $/\$ $\$ $\$
208	1, 207	sylan2 477	. . 3 $/\$ $\$ $\$
209	208	ralbidva 2826	. 2 $\$ $\$
210	56	iscmp 20415	. . 3 $/\$
211	210	baib 915	. 2
212	93	adantr 467	. . 3 $/\$ $\$
213		simpl 459	. . . . 5 $/\$
214		funmpt 5621	. . . . . 6 $\$
215	214	a1i 11	. . . . 5 $/\$ $\$
216		elpwi 3962	. . . . . . 7
217		foima 5803	. . . . . . . . 9 $\$ $\$
218	87, 217	syl 17	. . . . . . . 8 $\$
219	218	sseq2d 3462	. . . . . . 7 $\$
220	216, 219	syl5ibr 225	. . . . . 6 $\$
221	220	imp 431	. . . . 5 $/\$ $\$
222		ssimaexg 5936	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$
223	213, 215, 221, 222	syl3anc 1269	. . . 4 $/\$ $/\$ $\$
224		df-rex 2745	. . . . 5 $\$ $/\$ $\$
225		selpw 3960	. . . . . . 7
226	225	anbi1i 702	. . . . . 6 $/\$ $\$ $/\$ $\$
227	226	exbii 1720	. . . . 5 $/\$ $\$ $/\$ $\$
228	224, 227	bitri 253	. . . 4 $\$ $/\$ $\$
229	223, 228	sylibr 216	. . 3 $/\$ $\$
230		simpr 463	. . . . . . 7 $/\$ $\$ $\$
231	230	fveq2d 5874	. . . . . 6 $/\$ $\$ $\$
232	231	eleq2d 2516	. . . . 5 $/\$ $\$ $\$
233	232	notbid 296	. . . 4 $/\$ $\$ $\$
234	230	inteqd 4242	. . . . 5 $/\$ $\$ $\$
235	234	neeq1d 2685	. . . 4 $/\$ $\$ $\$
236	233, 235	imbi12d 322	. . 3 $/\$ $\$ $\$ $\$
237	212, 229, 236	ralxfrd 4617	. 2 $\$ $\$
238	209, 211, 237	3bitr4d 289	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371

wceq 1446

wex 1665

wcel 1889

wne 2624

wral 2739

wrex 2740

cvv 3047 $\$ cdif 3403

cun 3404

cin 3405

wss 3406

c0 3733

cpw 3953

csn 3970

cuni 4201

cint 4237

ciun 4281

ciin 4282

cmpt 4464

ccnv 4836

crn 4838

cres 4839

cima 4840

wfun 5579

wfn 5580

wfo 5583

wf1o 5584

cfv 5585

cfn 7574

cfi 7929

ctop 19929

ccld 20043

ccmp 20413

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-reu 2746 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-int 4238 df-iun 4283 df-iin 4284 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-2o 7188 df-oadd 7191 df-er 7368 df-map 7479 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-fi 7930 df-top 19933 df-cld 20046 df-cmp 20414

This theorem is referenced by: cmpfii 20436 fclscmp 21057 heibor1lem 32153

W3C validator