cmpfi - Metamath Proof Explorer

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

Theorem cmpfi 17425

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 3767	. . . 4
2		0ss 3616	. . . . . . . . . . 11
3		0fin 7295	. . . . . . . . . . 11
4		elfpw 7366	. . . . . . . . . . 11 $/\$
5	2, 3, 4	mpbir2an 887	. . . . . . . . . 10
6		simprr 734	. . . . . . . . . . 11 $/\$ $/\$ $/\$
7		simprl 733	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
8	7	unieqd 3986	. . . . . . . . . . 11 $/\$ $/\$ $/\$
9	6, 8	eqtrd 2436	. . . . . . . . . 10 $/\$ $/\$ $/\$
10		unieq 3984	. . . . . . . . . . . 12
11	10	eqeq2d 2415	. . . . . . . . . . 11
12	11	rspcev 3012	. . . . . . . . . 10 $/\$
13	5, 9, 12	sylancr 645	. . . . . . . . 9 $/\$ $/\$ $/\$
14	13	expr 599	. . . . . . . 8 $/\$ $/\$
15		vn0 3595	. . . . . . . . . 10
16		iineq1 4067	. . . . . . . . . . . . . 14 $\$ $\$
17	16	adantl 453	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
18		0iin 4109	. . . . . . . . . . . . 13 $\$
19	17, 18	syl6eq 2452	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20	19	eqeq1d 2412	. . . . . . . . . . 11 $/\$ $/\$ $\$
21	20	necon3bbid 2601	. . . . . . . . . 10 $/\$ $/\$ $\$
22	15, 21	mpbiri 225	. . . . . . . . 9 $/\$ $/\$ $\$
23	22	pm2.21d 100	. . . . . . . 8 $/\$ $/\$ $\$ $\$
24	14, 23	2thd 232	. . . . . . 7 $/\$ $/\$ $\$ $\$
25		uniss 3996	. . . . . . . . . . . 12
26	25	ad2antlr 708	. . . . . . . . . . 11 $/\$ $/\$
27		eqss 3323	. . . . . . . . . . . 12 $/\$
28	27	baib 872	. . . . . . . . . . 11
29	26, 28	syl 16	. . . . . . . . . 10 $/\$ $/\$
30		eqcom 2406	. . . . . . . . . 10
31		ssdif0 3646	. . . . . . . . . 10 $\$
32	29, 30, 31	3bitr3g 279	. . . . . . . . 9 $/\$ $/\$ $\$
33		iindif2 4120	. . . . . . . . . . . 12 $\$ $\$
34	33	adantl 453	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$
35		uniiun 4104	. . . . . . . . . . . 12
36	35	difeq2i 3422	. . . . . . . . . . 11 $\$ $\$
37	34, 36	syl6eqr 2454	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
38	37	eqeq1d 2412	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
39	32, 38	bitr4d 248	. . . . . . . 8 $/\$ $/\$ $\$
40		imassrn 5175	. . . . . . . . . . . 12 $\$ $\$
41		df-ima 4850	. . . . . . . . . . . . . 14 $\$ $\$
42		resmpt 5150	. . . . . . . . . . . . . . . 16 $\$ $\$
43	42	adantl 453	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
44	43	rneqd 5056	. . . . . . . . . . . . . 14 $/\$ $\$ $\$
45	41, 44	syl5eq 2448	. . . . . . . . . . . . 13 $/\$ $\$ $\$
46	45	ad2antrr 707	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
47	40, 46	syl5sseqr 3357	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
48		funmpt 5448	. . . . . . . . . . . 12 $\$
49		elfpw 7366	. . . . . . . . . . . . . 14 $/\$
50	49	simprbi 451	. . . . . . . . . . . . 13
51	50	adantl 453	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
52		imafi 7357	. . . . . . . . . . . 12 $\$ $/\$ $\$
53	48, 51, 52	sylancr 645	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$
54		elfpw 7366	. . . . . . . . . . 11 $\$ $\$ $\$ $\$ $/\$ $\$
55	47, 53, 54	sylanbrc 646	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
56		eqid 2404	. . . . . . . . . . . . . . . . 17
57	56	topopn 16934	. . . . . . . . . . . . . . . 16
58		difexg 4311	. . . . . . . . . . . . . . . 16 $\$
59	57, 58	syl 16	. . . . . . . . . . . . . . 15 $\$
60	59	ralrimivw 2750	. . . . . . . . . . . . . 14 $\$
61		eqid 2404	. . . . . . . . . . . . . . 15 $\$ $\$
62	61	fnmpt 5530	. . . . . . . . . . . . . 14 $\$ $\$
63	60, 62	syl 16	. . . . . . . . . . . . 13 $\$
64	63	ad3antrrr 711	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
65		simpr 448	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$
66		elfpw 7366	. . . . . . . . . . . . . . 15 $\$ $\$ $/\$
67	65, 66	sylib 189	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$ $/\$
68	67	simpld 446	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
69	45	ad2antrr 707	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$ $\$
70	68, 69	sseqtrd 3344	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
71	67	simprd 450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
72		fipreima 7370	. . . . . . . . . . . 12 $\$ $/\$ $\$ $/\$ $\$
73	64, 70, 71, 72	syl3anc 1184	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
74		eqcom 2406	. . . . . . . . . . . 12 $\$ $\$
75	74	rexbii 2691	. . . . . . . . . . 11 $\$ $\$
76	73, 75	sylib 189	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
77		simpr 448	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
78	77	inteqd 4015	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $\$ $\$
79	78	eqeq2d 2415	. . . . . . . . . 10 $/\$ $/\$ $/\$ $\$ $\$
80	55, 76, 79	rexxfrd 4697	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
81		0ex 4299	. . . . . . . . . 10
82		imassrn 5175	. . . . . . . . . . . . 13 $\$ $\$
83		eqid 2404	. . . . . . . . . . . . . . . . 17 $\$ $\$
84	56, 83	opncldf1 17103	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$
85	84	simpld 446	. . . . . . . . . . . . . . 15 $\$
86		f1ofo 5640	. . . . . . . . . . . . . . 15 $\$ $\$
87	85, 86	syl 16	. . . . . . . . . . . . . 14 $\$
88		forn 5615	. . . . . . . . . . . . . 14 $\$ $\$
89	87, 88	syl 16	. . . . . . . . . . . . 13 $\$
90	82, 89	syl5sseq 3356	. . . . . . . . . . . 12 $\$
91		fvex 5701	. . . . . . . . . . . . 13
92	91	elpw2 4324	. . . . . . . . . . . 12 $\$ $\$
93	90, 92	sylibr 204	. . . . . . . . . . 11 $\$
94	93	ad2antrr 707	. . . . . . . . . 10 $/\$ $/\$ $\$
95		elfi 7376	. . . . . . . . . 10 $/\$ $\$ $\$ $\$
96	81, 94, 95	sylancr 645	. . . . . . . . 9 $/\$ $/\$ $\$ $\$
97		inundif 3666	. . . . . . . . . . . . . 14 $\$
98	97	rexeqi 2869	. . . . . . . . . . . . 13 $\$
99		rexun 3487	. . . . . . . . . . . . 13 $\$ $\/$ $\$
100	98, 99	bitr3i 243	. . . . . . . . . . . 12 $\/$ $\$
101		inss2 3522	. . . . . . . . . . . . . . . . . . . . . 22
102	101	sseli 3304	. . . . . . . . . . . . . . . . . . . . 21
103		elsni 3798	. . . . . . . . . . . . . . . . . . . . 21
104	102, 103	syl 16	. . . . . . . . . . . . . . . . . . . 20
105	104	unieqd 3986	. . . . . . . . . . . . . . . . . . 19
106		uni0 4002	. . . . . . . . . . . . . . . . . . 19
107	105, 106	syl6eq 2452	. . . . . . . . . . . . . . . . . 18
108	107	eqeq2d 2415	. . . . . . . . . . . . . . . . 17
109	108	biimpd 199	. . . . . . . . . . . . . . . 16
110	109	rexlimiv 2784	. . . . . . . . . . . . . . 15
111		ssid 3327	. . . . . . . . . . . . . . . . . . . 20
112	111	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
113		simprr 734	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
114		0ss 3616	. . . . . . . . . . . . . . . . . . . . . . . . 25
115	113, 114	syl6eqss 3358	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
116	25	ad2antlr 708	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
117	115, 116	eqssd 3325	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
118	117, 113	eqtr3d 2438	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
119	118, 3	syl6eqel 2492	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
120		pwfi 7360	. . . . . . . . . . . . . . . . . . . . 21
121	119, 120	sylib 189	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
122		pwuni 4355	. . . . . . . . . . . . . . . . . . . 20
123		ssfi 7288	. . . . . . . . . . . . . . . . . . . 20 $/\$
124	121, 122, 123	sylancl 644	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
125		elfpw 7366	. . . . . . . . . . . . . . . . . . 19 $/\$
126	112, 124, 125	sylanbrc 646	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
127		simprl 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
128		eldifsn 3887	. . . . . . . . . . . . . . . . . 18 $\$ $/\$
129	126, 127, 128	sylanbrc 646	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
130		unieq 3984	. . . . . . . . . . . . . . . . . . 19
131	130	eqeq2d 2415	. . . . . . . . . . . . . . . . . 18
132	131	rspcev 3012	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$
133	129, 117, 132	syl2anc 643	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
134	133	expr 599	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
135	110, 134	syl5 30	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
136		idd 22	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
137	135, 136	jaod 370	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $\$ $\$
138		olc 374	. . . . . . . . . . . . 13 $\$ $\/$ $\$
139	137, 138	impbid1 195	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $\$ $\$
140	100, 139	syl5bb 249	. . . . . . . . . . 11 $/\$ $/\$ $\$
141		eldifi 3429	. . . . . . . . . . . . . . . . . . . 20 $\$
142	141	adantl 453	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$
143	142, 49	sylib 189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$ $/\$
144	143	simpld 446	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
145		simpllr 736	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
146	144, 145	sstrd 3318	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
147	146	unissd 3999	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
148		eqss 3323	. . . . . . . . . . . . . . . 16 $/\$
149	148	baib 872	. . . . . . . . . . . . . . 15
150	147, 149	syl 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
151		eqcom 2406	. . . . . . . . . . . . . 14
152		ssdif0 3646	. . . . . . . . . . . . . . 15 $\$
153		eqcom 2406	. . . . . . . . . . . . . . 15 $\$ $\$
154	152, 153	bitri 241	. . . . . . . . . . . . . 14 $\$
155	150, 151, 154	3bitr3g 279	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
156		df-ima 4850	. . . . . . . . . . . . . . . . . 18 $\$ $\$
157		resmpt 5150	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
158	144, 157	syl 16	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $\$ $\$ $\$
159	158	rneqd 5056	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $\$ $\$ $\$
160	156, 159	syl5eq 2448	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $\$ $\$
161	160	inteqd 4015	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
162	59	ralrimivw 2750	. . . . . . . . . . . . . . . . . 18 $\$
163	162	ad3antrrr 711	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$ $\$
164		dfiin3g 5082	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
165	163, 164	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
166		eldifsn 3887	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
167	166	simprbi 451	. . . . . . . . . . . . . . . . . 18 $\$
168	167	adantl 453	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
169		iindif2 4120	. . . . . . . . . . . . . . . . 17 $\$ $\$
170	168, 169	syl 16	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$ $\$ $\$
171	161, 165, 170	3eqtr2d 2442	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$ $\$ $\$
172		uniiun 4104	. . . . . . . . . . . . . . . 16
173	172	difeq2i 3422	. . . . . . . . . . . . . . 15 $\$ $\$
174	171, 173	syl6eqr 2454	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$ $\$
175	174	eqeq2d 2415	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$ $\$
176	155, 175	bitr4d 248	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$ $\$
177	176	rexbidva 2683	. . . . . . . . . . 11 $/\$ $/\$ $\$ $\$ $\$
178	140, 177	bitrd 245	. . . . . . . . . 10 $/\$ $/\$ $\$ $\$
179		imaeq2 5158	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
180		ima0 5180	. . . . . . . . . . . . . . . . . . . 20 $\$
181	179, 180	syl6eq 2452	. . . . . . . . . . . . . . . . . . 19 $\$
182	181	inteqd 4015	. . . . . . . . . . . . . . . . . 18 $\$
183		int0 4024	. . . . . . . . . . . . . . . . . 18
184	182, 183	syl6eq 2452	. . . . . . . . . . . . . . . . 17 $\$
185	184	neeq1d 2580	. . . . . . . . . . . . . . . 16 $\$
186	15, 185	mpbiri 225	. . . . . . . . . . . . . . 15 $\$
187	186	necomd 2650	. . . . . . . . . . . . . 14 $\$
188	187	necon2i 2614	. . . . . . . . . . . . 13 $\$
189	166	rbaibr 875	. . . . . . . . . . . . 13 $\$
190	188, 189	syl 16	. . . . . . . . . . . 12 $\$ $\$
191	190	pm5.32ri 620	. . . . . . . . . . 11 $/\$ $\$ $\$ $/\$ $\$
192	191	rexbii2 2695	. . . . . . . . . 10 $\$ $\$ $\$
193	178, 192	syl6bbr 255	. . . . . . . . 9 $/\$ $/\$ $\$
194	80, 96, 193	3bitr4rd 278	. . . . . . . 8 $/\$ $/\$ $\$
195	39, 194	imbi12d 312	. . . . . . 7 $/\$ $/\$ $\$ $\$
196	24, 195	pm2.61dane 2645	. . . . . 6 $/\$ $\$ $\$
197	60	adantr 452	. . . . . . . . . . 11 $/\$ $\$
198		dfiin3g 5082	. . . . . . . . . . 11 $\$ $\$ $\$
199	197, 198	syl 16	. . . . . . . . . 10 $/\$ $\$ $\$
200	45	inteqd 4015	. . . . . . . . . 10 $/\$ $\$ $\$
201	199, 200	eqtr4d 2439	. . . . . . . . 9 $/\$ $\$ $\$
202	201	eqeq1d 2412	. . . . . . . 8 $/\$ $\$ $\$
203		nne 2571	. . . . . . . 8 $\$ $\$
204	202, 203	syl6bbr 255	. . . . . . 7 $/\$ $\$ $\$
205	204	imbi1d 309	. . . . . 6 $/\$ $\$ $\$ $\$ $\$
206	196, 205	bitrd 245	. . . . 5 $/\$ $\$ $\$
207		con1b 324	. . . . 5 $\$ $\$ $\$ $\$
208	206, 207	syl6bb 253	. . . 4 $/\$ $\$ $\$
209	1, 208	sylan2 461	. . 3 $/\$ $\$ $\$
210	209	ralbidva 2682	. 2 $\$ $\$
211	56	iscmp 17405	. . 3 $/\$
212	211	baib 872	. 2
213	93	adantr 452	. . 3 $/\$ $\$
214		simpl 444	. . . . 5 $/\$
215		funmpt 5448	. . . . . 6 $\$
216	215	a1i 11	. . . . 5 $/\$ $\$
217		elpwi 3767	. . . . . . 7
218		foima 5617	. . . . . . . . 9 $\$ $\$
219	87, 218	syl 16	. . . . . . . 8 $\$
220	219	sseq2d 3336	. . . . . . 7 $\$
221	217, 220	syl5ibr 213	. . . . . 6 $\$
222	221	imp 419	. . . . 5 $/\$ $\$
223		ssimaexg 5748	. . . . 5 $/\$ $\$ $/\$ $\$ $/\$ $\$
224	214, 216, 222, 223	syl3anc 1184	. . . 4 $/\$ $/\$ $\$
225		df-rex 2672	. . . . 5 $\$ $/\$ $\$
226		vex 2919	. . . . . . . 8
227	226	elpw 3765	. . . . . . 7
228	227	anbi1i 677	. . . . . 6 $/\$ $\$ $/\$ $\$
229	228	exbii 1589	. . . . 5 $/\$ $\$ $/\$ $\$
230	225, 229	bitri 241	. . . 4 $\$ $/\$ $\$
231	224, 230	sylibr 204	. . 3 $/\$ $\$
232		simpr 448	. . . . . . 7 $/\$ $\$ $\$
233	232	fveq2d 5691	. . . . . 6 $/\$ $\$ $\$
234	233	eleq2d 2471	. . . . 5 $/\$ $\$ $\$
235	234	notbid 286	. . . 4 $/\$ $\$ $\$
236	232	inteqd 4015	. . . . 5 $/\$ $\$ $\$
237	236	neeq1d 2580	. . . 4 $/\$ $\$ $\$
238	235, 237	imbi12d 312	. . 3 $/\$ $\$ $\$ $\$
239	213, 231, 238	ralxfrd 4696	. 2 $\$ $\$
240	210, 212, 239	3bitr4d 277	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $\/$ wo 358 $/\$ wa 359

wex 1547

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cvv 2916 $\$ cdif 3277

cun 3278

cin 3279

wss 3280

c0 3588

cpw 3759

csn 3774

cuni 3975

cint 4010

ciun 4053

ciin 4054

cmpt 4226

ccnv 4836

crn 4838

cres 4839

cima 4840

wfun 5407

wfn 5408

wfo 5411

wf1o 5412

cfv 5413

cfn 7068

cfi 7373

ctop 16913

ccld 17035

ccmp 17403

This theorem is referenced by: cmpfii 17426 fclscmp 18015 heibor1lem 26408

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-ral 2671 df-rex 2672 df-reu 2673 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-iin 4056 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 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-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-recs 6592 df-rdg 6627 df-1o 6683 df-2o 6684 df-oadd 6687 df-er 6864 df-map 6979 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-fi 7374 df-top 16918 df-cld 17038 df-cmp 17404

W3C validator