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 20500

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 3951	. . . 4
2		0ss 3766	. . . . . . . . . . 11
3		0fin 7817	. . . . . . . . . . 11
4		elfpw 7894	. . . . . . . . . . 11 $/\$
5	2, 3, 4	mpbir2an 934	. . . . . . . . . 10
6		simprr 774	. . . . . . . . . . 11 $/\$ $/\$ $/\$
7		simprl 772	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
8	7	unieqd 4200	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	6, 8	eqtrd 2505	. . . . . . . . . 10 $/\$ $/\$ $/\$
10		unieq 4198	. . . . . . . . . . . 12
11	10	eqeq2d 2481	. . . . . . . . . . 11
12	11	rspcev 3136	. . . . . . . . . 10 $/\$
13	5, 9, 12	sylancr 676	. . . . . . . . 9 $/\$ $/\$ $/\$
14	13	expr 626	. . . . . . . 8 $/\$ $/\$
15		vn0 3730	. . . . . . . . . 10
16		iineq1 4284	. . . . . . . . . . . . . 14 $\$ $\$
17	16	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
18		0iin 4327	. . . . . . . . . . . . 13 $\$
19	17, 18	syl6eq 2521	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20	19	eqeq1d 2473	. . . . . . . . . . 11 $/\$ $/\$ $\$
21	20	necon3bbid 2680	. . . . . . . . . 10 $/\$ $/\$ $\$
22	15, 21	mpbiri 241	. . . . . . . . 9 $/\$ $/\$ $\$
23	22	pm2.21d 109	. . . . . . . 8 $/\$ $/\$ $\$ $\$
24	14, 23	2thd 248	. . . . . . 7 $/\$ $/\$ $\$ $\$
25		uniss 4211	. . . . . . . . . . . 12
26	25	ad2antlr 741	. . . . . . . . . . 11 $/\$ $/\$
27		eqss 3433	. . . . . . . . . . . 12 $/\$
28	27	baib 919	. . . . . . . . . . 11
29	26, 28	syl 17	. . . . . . . . . 10 $/\$ $/\$
30		eqcom 2478	. . . . . . . . . 10
31		ssdif0 3741	. . . . . . . . . 10 $\$
32	29, 30, 31	3bitr3g 295	. . . . . . . . 9 $/\$ $/\$ $\$
33		iindif2 4338	. . . . . . . . . . . 12 $\$ $\$
34	33	adantl 473	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
35		uniiun 4322	. . . . . . . . . . . 12
36	35	difeq2i 3537	. . . . . . . . . . 11 $\$ $\$
37	34, 36	syl6eqr 2523	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
38	37	eqeq1d 2473	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
39	32, 38	bitr4d 264	. . . . . . . 8 $/\$ $/\$ $\$
40		imassrn 5185	. . . . . . . . . . . 12 $\$ $\$
41		df-ima 4852	. . . . . . . . . . . . . 14 $\$ $\$
42		resmpt 5160	. . . . . . . . . . . . . . . 16 $\$ $\$
43	42	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
44	43	rneqd 5068	. . . . . . . . . . . . . 14 $/\$ $\$ $\$
45	41, 44	syl5eq 2517	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46	45	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
47	40, 46	syl5sseqr 3467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
48		funmpt 5625	. . . . . . . . . . . 12 $\$
49		elfpw 7894	. . . . . . . . . . . . . 14 $/\$
50	49	simprbi 471	. . . . . . . . . . . . 13
51	50	adantl 473	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
52		imafi 7885	. . . . . . . . . . . 12 $\$ $/\$ $\$
53	48, 51, 52	sylancr 676	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
54		elfpw 7894	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $/\$ $\$
55	47, 53, 54	sylanbrc 677	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
56		eqid 2471	. . . . . . . . . . . . . . . . 17
57	56	topopn 20013	. . . . . . . . . . . . . . . 16
58		difexg 4545	. . . . . . . . . . . . . . . 16 $\$
59	57, 58	syl 17	. . . . . . . . . . . . . . 15 $\$
60	59	ralrimivw 2810	. . . . . . . . . . . . . 14 $\$
61		eqid 2471	. . . . . . . . . . . . . . 15 $\$ $\$
62	61	fnmpt 5714	. . . . . . . . . . . . . 14 $\$ $\$
63	60, 62	syl 17	. . . . . . . . . . . . 13 $\$
64	63	ad3antrrr 744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
65		simpr 468	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$
66		elfpw 7894	. . . . . . . . . . . . . . 15 $\$ $\$ $/\$
67	65, 66	sylib 201	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$ $/\$
68	67	simpld 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
69	45	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$ $\$
70	68, 69	sseqtrd 3454	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
71	67	simprd 470	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
72		fipreima 7898	. . . . . . . . . . . 12 $\$ $/\$ $\$ $/\$ $\$
73	64, 70, 71, 72	syl3anc 1292	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
74		eqcom 2478	. . . . . . . . . . . 12 $\$ $\$
75	74	rexbii 2881	. . . . . . . . . . 11 $\$ $\$
76	73, 75	sylib 201	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
77		simpr 468	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
78	77	inteqd 4231	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
79	78	eqeq2d 2481	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
80	55, 76, 79	rexxfrd 4613	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
81		0ex 4528	. . . . . . . . . 10
82		imassrn 5185	. . . . . . . . . . . . 13 $\$ $\$
83		eqid 2471	. . . . . . . . . . . . . . . . 17 $\$ $\$
84	56, 83	opncldf1 20177	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$
85	84	simpld 466	. . . . . . . . . . . . . . 15 $\$
86		f1ofo 5835	. . . . . . . . . . . . . . 15 $\$ $\$
87	85, 86	syl 17	. . . . . . . . . . . . . 14 $\$
88		forn 5809	. . . . . . . . . . . . . 14 $\$ $\$
89	87, 88	syl 17	. . . . . . . . . . . . 13 $\$
90	82, 89	syl5sseq 3466	. . . . . . . . . . . 12 $\$
91		fvex 5889	. . . . . . . . . . . . 13
92	91	elpw2 4565	. . . . . . . . . . . 12 $\$ $\$
93	90, 92	sylibr 217	. . . . . . . . . . 11 $\$
94	93	ad2antrr 740	. . . . . . . . . 10 $/\$ $/\$ $\$
95		elfi 7945	. . . . . . . . . 10 $/\$ $\$ $\$ $\$
96	81, 94, 95	sylancr 676	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
97		inundif 3836	. . . . . . . . . . . . . 14 $\$
98	97	rexeqi 2978	. . . . . . . . . . . . 13 $\$
99		rexun 3605	. . . . . . . . . . . . 13 $\$ $\/$ $\$
100	98, 99	bitr3i 259	. . . . . . . . . . . 12 $\/$ $\$
101		inss2 3644	. . . . . . . . . . . . . . . . . . . . . 22
102	101	sseli 3414	. . . . . . . . . . . . . . . . . . . . 21
103		elsni 3985	. . . . . . . . . . . . . . . . . . . . 21
104	102, 103	syl 17	. . . . . . . . . . . . . . . . . . . 20
105	104	unieqd 4200	. . . . . . . . . . . . . . . . . . 19
106		uni0 4217	. . . . . . . . . . . . . . . . . . 19
107	105, 106	syl6eq 2521	. . . . . . . . . . . . . . . . . 18
108	107	eqeq2d 2481	. . . . . . . . . . . . . . . . 17
109	108	biimpd 212	. . . . . . . . . . . . . . . 16
110	109	rexlimiv 2867	. . . . . . . . . . . . . . 15
111		ssid 3437	. . . . . . . . . . . . . . . . . . . 20
112	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
113		simprr 774	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
114		0ss 3766	. . . . . . . . . . . . . . . . . . . . . . . . 25
115	113, 114	syl6eqss 3468	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
116	25	ad2antlr 741	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
117	115, 116	eqssd 3435	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
118	117, 113	eqtr3d 2507	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
119	118, 3	syl6eqel 2557	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
120		pwfi 7887	. . . . . . . . . . . . . . . . . . . . 21
121	119, 120	sylib 201	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
122		pwuni 4631	. . . . . . . . . . . . . . . . . . . 20
123		ssfi 7810	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	121, 122, 123	sylancl 675	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
125		elfpw 7894	. . . . . . . . . . . . . . . . . . 19 $/\$
126	112, 124, 125	sylanbrc 677	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
127		simprl 772	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
128		eldifsn 4088	. . . . . . . . . . . . . . . . . 18 $\$ $/\$
129	126, 127, 128	sylanbrc 677	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
130		unieq 4198	. . . . . . . . . . . . . . . . . . 19
131	130	eqeq2d 2481	. . . . . . . . . . . . . . . . . 18
132	131	rspcev 3136	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$
133	129, 117, 132	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
134	133	expr 626	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
135	110, 134	syl5 32	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
136		idd 24	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
137	135, 136	jaod 387	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $\$ $\$
138		olc 391	. . . . . . . . . . . . 13 $\$ $\/$ $\$
139	137, 138	impbid1 208	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $\$ $\$
140	100, 139	syl5bb 265	. . . . . . . . . . 11 $/\$ $/\$ $\$
141		eldifi 3544	. . . . . . . . . . . . . . . . . . . 20 $\$
142	141	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
143	142, 49	sylib 201	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$ $/\$
144	143	simpld 466	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
145		simpllr 777	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
146	144, 145	sstrd 3428	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
147	146	unissd 4214	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
148		eqss 3433	. . . . . . . . . . . . . . . 16 $/\$
149	148	baib 919	. . . . . . . . . . . . . . 15
150	147, 149	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
151		eqcom 2478	. . . . . . . . . . . . . 14
152		ssdif0 3741	. . . . . . . . . . . . . . 15 $\$
153		eqcom 2478	. . . . . . . . . . . . . . 15 $\$ $\$
154	152, 153	bitri 257	. . . . . . . . . . . . . 14 $\$
155	150, 151, 154	3bitr3g 295	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
156		df-ima 4852	. . . . . . . . . . . . . . . . . 18 $\$ $\$
157	144	resmptd 5162	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$ $\$ $\$
158	157	rneqd 5068	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$ $\$ $\$
159	156, 158	syl5eq 2517	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $\$ $\$
160	159	inteqd 4231	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
161	59	ralrimivw 2810	. . . . . . . . . . . . . . . . . 18 $\$
162	161	ad3antrrr 744	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $\$
163		dfiin3g 5094	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
164	162, 163	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
165		eldifsn 4088	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
166	165	simprbi 471	. . . . . . . . . . . . . . . . . 18 $\$
167	166	adantl 473	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
168		iindif2 4338	. . . . . . . . . . . . . . . . 17 $\$ $\$
169	167, 168	syl 17	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
170	160, 164, 169	3eqtr2d 2511	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$ $\$
171		uniiun 4322	. . . . . . . . . . . . . . . 16
172	171	difeq2i 3537	. . . . . . . . . . . . . . 15 $\$ $\$
173	170, 172	syl6eqr 2523	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$ $\$
174	173	eqeq2d 2481	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$ $\$
175	155, 174	bitr4d 264	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
176	175	rexbidva 2889	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$ $\$
177	140, 176	bitrd 261	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
178		imaeq2 5170	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
179		ima0 5189	. . . . . . . . . . . . . . . . . . . 20 $\$
180	178, 179	syl6eq 2521	. . . . . . . . . . . . . . . . . . 19 $\$
181	180	inteqd 4231	. . . . . . . . . . . . . . . . . 18 $\$
182		int0 4240	. . . . . . . . . . . . . . . . . 18
183	181, 182	syl6eq 2521	. . . . . . . . . . . . . . . . 17 $\$
184	183	neeq1d 2702	. . . . . . . . . . . . . . . 16 $\$
185	15, 184	mpbiri 241	. . . . . . . . . . . . . . 15 $\$
186	185	necomd 2698	. . . . . . . . . . . . . 14 $\$
187	186	necon2i 2677	. . . . . . . . . . . . 13 $\$
188	165	rbaibr 921	. . . . . . . . . . . . 13 $\$
189	187, 188	syl 17	. . . . . . . . . . . 12 $\$ $\$
190	189	pm5.32ri 650	. . . . . . . . . . 11 $/\$ $\$ $\$ $/\$ $\$
191	190	rexbii2 2879	. . . . . . . . . 10 $\$ $\$ $\$
192	177, 191	syl6bbr 271	. . . . . . . . 9 $/\$ $/\$ $\$
193	80, 96, 192	3bitr4rd 294	. . . . . . . 8 $/\$ $/\$ $\$
194	39, 193	imbi12d 327	. . . . . . 7 $/\$ $/\$ $\$ $\$
195	24, 194	pm2.61dane 2730	. . . . . 6 $/\$ $\$ $\$
196	60	adantr 472	. . . . . . . . . . 11 $/\$ $\$
197		dfiin3g 5094	. . . . . . . . . . 11 $\$ $\$ $\$
198	196, 197	syl 17	. . . . . . . . . 10 $/\$ $\$ $\$
199	45	inteqd 4231	. . . . . . . . . 10 $/\$ $\$ $\$
200	198, 199	eqtr4d 2508	. . . . . . . . 9 $/\$ $\$ $\$
201	200	eqeq1d 2473	. . . . . . . 8 $/\$ $\$ $\$
202		nne 2647	. . . . . . . 8 $\$ $\$
203	201, 202	syl6bbr 271	. . . . . . 7 $/\$ $\$ $\$
204	203	imbi1d 324	. . . . . 6 $/\$ $\$ $\$ $\$ $\$
205	195, 204	bitrd 261	. . . . 5 $/\$ $\$ $\$
206		con1b 340	. . . . 5 $\$ $\$ $\$ $\$
207	205, 206	syl6bb 269	. . . 4 $/\$ $\$ $\$
208	1, 207	sylan2 482	. . 3 $/\$ $\$ $\$
209	208	ralbidva 2828	. 2 $\$ $\$
210	56	iscmp 20480	. . 3 $/\$
211	210	baib 919	. 2
212	93	adantr 472	. . 3 $/\$ $\$
213		simpl 464	. . . . 5 $/\$
214		funmpt 5625	. . . . . 6 $\$
215	214	a1i 11	. . . . 5 $/\$ $\$
216		elpwi 3951	. . . . . . 7
217		foima 5811	. . . . . . . . 9 $\$ $\$
218	87, 217	syl 17	. . . . . . . 8 $\$
219	218	sseq2d 3446	. . . . . . 7 $\$
220	216, 219	syl5ibr 229	. . . . . 6 $\$
221	220	imp 436	. . . . 5 $/\$ $\$
222		ssimaexg 5946	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$
223	213, 215, 221, 222	syl3anc 1292	. . . 4 $/\$ $/\$ $\$
224		df-rex 2762	. . . . 5 $\$ $/\$ $\$
225		selpw 3949	. . . . . . 7
226	225	anbi1i 709	. . . . . 6 $/\$ $\$ $/\$ $\$
227	226	exbii 1726	. . . . 5 $/\$ $\$ $/\$ $\$
228	224, 227	bitri 257	. . . 4 $\$ $/\$ $\$
229	223, 228	sylibr 217	. . 3 $/\$ $\$
230		simpr 468	. . . . . . 7 $/\$ $\$ $\$
231	230	fveq2d 5883	. . . . . 6 $/\$ $\$ $\$
232	231	eleq2d 2534	. . . . 5 $/\$ $\$ $\$
233	232	notbid 301	. . . 4 $/\$ $\$ $\$
234	230	inteqd 4231	. . . . 5 $/\$ $\$ $\$
235	234	neeq1d 2702	. . . 4 $/\$ $\$ $\$
236	233, 235	imbi12d 327	. . 3 $/\$ $\$ $\$ $\$
237	212, 229, 236	ralxfrd 4612	. 2 $\$ $\$
238	209, 211, 237	3bitr4d 293	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376

wceq 1452

wex 1671

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031 $\$ cdif 3387

cun 3388

cin 3389

wss 3390

c0 3722

cpw 3942

csn 3959

cuni 4190

cint 4226

ciun 4269

ciin 4270

cmpt 4454

ccnv 4838

crn 4840

cres 4841

cima 4842

wfun 5583

wfn 5584

wfo 5587

wf1o 5588

cfv 5589

cfn 7587

cfi 7942

ctop 19994

ccld 20108

ccmp 20478

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-2o 7201 df-oadd 7204 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-fi 7943 df-top 19998 df-cld 20111 df-cmp 20479

This theorem is referenced by: cmpfii 20501 fclscmp 21123 heibor1lem 32205

W3C validator