disjinfi - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > disjinfi		Structured version Visualization version Unicode version

Theorem disjinfi 37539

Description: Only a finite number of disjoint sets can have a non empty intersection with a finite set

(Contributed by Glauco Siliprandi, 17-Aug-2020.)

**Hypotheses**
Ref	Expression
disjinfi.b	$/\$
disjinfi.d	Disj
disjinfi.c

**Assertion**
Ref	Expression
disjinfi

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem disjinfi Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		disjinfi.c	. . 3
2		id 22	. . . 4
3		inss2 3644	. . . . 5
4	3	a1i 11	. . . 4
5		ssfi 7810	. . . 4 $/\$
6	2, 4, 5	syl2anc 673	. . 3
7	1, 6	syl 17	. 2
8	3	a1i 11	. . . . 5
9	8, 1	jca 541	. . . 4 $/\$
10		ssexg 4542	. . . 4 $/\$
11	9, 10	syl 17	. . 3
12		elinel1 3610	. . . . . . . . . . . . 13
13		eluni2 4194	. . . . . . . . . . . . . . 15
14	13	biimpi 199	. . . . . . . . . . . . . 14
15		vex 3034	. . . . . . . . . . . . . . . . . . . . 21
16		eqid 2471	. . . . . . . . . . . . . . . . . . . . . 22
17	16	elrnmpt 5087	. . . . . . . . . . . . . . . . . . . . 21
18	15, 17	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20
19	18	biimpi 199	. . . . . . . . . . . . . . . . . . 19
20	19	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
21		nfcv 2612	. . . . . . . . . . . . . . . . . . . . 21
22		nfmpt1 4485	. . . . . . . . . . . . . . . . . . . . . 22
23	22	nfrn 5083	. . . . . . . . . . . . . . . . . . . . 21
24	21, 23	nfel 2624	. . . . . . . . . . . . . . . . . . . 20
25		nfv 1769	. . . . . . . . . . . . . . . . . . . 20
26	24, 25	nfan 2031	. . . . . . . . . . . . . . . . . . 19 $/\$
27		simpl 464	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
28		simpr 468	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
29	27, 28	eleqtrd 2551	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
30	29	ex 441	. . . . . . . . . . . . . . . . . . . . 21
31	30	a1d 25	. . . . . . . . . . . . . . . . . . . 20
32	31	adantl 473	. . . . . . . . . . . . . . . . . . 19 $/\$
33	26, 32	reximdai 2853	. . . . . . . . . . . . . . . . . 18 $/\$
34	20, 33	mpd 15	. . . . . . . . . . . . . . . . 17 $/\$
35	34	ex 441	. . . . . . . . . . . . . . . 16
36	35	a1i 11	. . . . . . . . . . . . . . 15
37	36	rexlimdv 2870	. . . . . . . . . . . . . 14
38	14, 37	mpd 15	. . . . . . . . . . . . 13
39	12, 38	syl 17	. . . . . . . . . . . 12
40	39	adantl 473	. . . . . . . . . . 11 $/\$
41		nfv 1769	. . . . . . . . . . . . 13
42		nfcv 2612	. . . . . . . . . . . . . 14
43	23	nfuni 4196	. . . . . . . . . . . . . . 15
44		nfcv 2612	. . . . . . . . . . . . . . 15
45	43, 44	nfin 3630	. . . . . . . . . . . . . 14
46	42, 45	nfel 2624	. . . . . . . . . . . . 13
47	41, 46	nfan 2031	. . . . . . . . . . . 12 $/\$
48		nfre1 2846	. . . . . . . . . . . 12
49	3	sseli 3414	. . . . . . . . . . . . . 14
50		simp2 1031	. . . . . . . . . . . . . . . 16 $/\$ $/\$
51		simpr 468	. . . . . . . . . . . . . . . . . 18 $/\$
52		simpl 464	. . . . . . . . . . . . . . . . . 18 $/\$
53	51, 52	elind 3609	. . . . . . . . . . . . . . . . 17 $/\$
54	53	3adant2 1049	. . . . . . . . . . . . . . . 16 $/\$ $/\$
55		rspe 2844	. . . . . . . . . . . . . . . 16 $/\$
56	50, 54, 55	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$
57	56	3exp 1230	. . . . . . . . . . . . . 14
58	49, 57	syl 17	. . . . . . . . . . . . 13
59	58	adantl 473	. . . . . . . . . . . 12 $/\$
60	47, 48, 59	rexlimd 2866	. . . . . . . . . . 11 $/\$
61	40, 60	mpd 15	. . . . . . . . . 10 $/\$
62		disjinfi.d	. . . . . . . . . . . . . . . . . . . . 21 Disj
63		disjors 4381	. . . . . . . . . . . . . . . . . . . . 21 Disj $\/$
64	62, 63	sylib 201	. . . . . . . . . . . . . . . . . . . 20 $\/$
65		nfv 1769	. . . . . . . . . . . . . . . . . . . . 21 $\/$
66		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . 22
67		nfv 1769	. . . . . . . . . . . . . . . . . . . . . . 23
68		nfcsb1v 3365	. . . . . . . . . . . . . . . . . . . . . . . . 25
69	21	nfcsb1 3364	. . . . . . . . . . . . . . . . . . . . . . . . 25
70	68, 69	nfin 3630	. . . . . . . . . . . . . . . . . . . . . . . 24
71		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . . . 24
72	70, 71	nfeq 2623	. . . . . . . . . . . . . . . . . . . . . . 23
73	67, 72	nfor 2038	. . . . . . . . . . . . . . . . . . . . . 22 $\/$
74	66, 73	nfral 2789	. . . . . . . . . . . . . . . . . . . . 21 $\/$
75		eqeq1 2475	. . . . . . . . . . . . . . . . . . . . . . 23
76		csbeq1a 3358	. . . . . . . . . . . . . . . . . . . . . . . . 25
77	76	ineq1d 3624	. . . . . . . . . . . . . . . . . . . . . . . 24
78	77	eqeq1d 2473	. . . . . . . . . . . . . . . . . . . . . . 23
79	75, 78	orbi12d 724	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $\/$
80	79	ralbidv 2829	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $\/$
81	65, 74, 80	cbvral 3001	. . . . . . . . . . . . . . . . . . . 20 $\/$ $\/$
82	64, 81	sylibr 217	. . . . . . . . . . . . . . . . . . 19 $\/$
83		rspa 2774	. . . . . . . . . . . . . . . . . . 19 $\/$ $/\$ $\/$
84	82, 83	sylan 479	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
85	84	adantr 472	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
86		simpr 468	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
87		rspa 2774	. . . . . . . . . . . . . . . . . 18 $\/$ $/\$ $\/$
88	87	orcomd 395	. . . . . . . . . . . . . . . . 17 $\/$ $/\$ $\/$
89	85, 86, 88	syl2anc 673	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
90	89	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\/$
91		elinel1 3610	. . . . . . . . . . . . . . . . . . 19
92	91	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$
93		sbsbc 3259	. . . . . . . . . . . . . . . . . . . . . 22
94		sbcel2 3782	. . . . . . . . . . . . . . . . . . . . . 22
95		csbin 3803	. . . . . . . . . . . . . . . . . . . . . . 23
96	95	eleq2i 2541	. . . . . . . . . . . . . . . . . . . . . 22
97	93, 94, 96	3bitri 279	. . . . . . . . . . . . . . . . . . . . 21
98	97	biimpi 199	. . . . . . . . . . . . . . . . . . . 20
99		elinel1 3610	. . . . . . . . . . . . . . . . . . . 20
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . 19
101	100	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$
102	92, 101	jca 541	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
103		inelcm 3823	. . . . . . . . . . . . . . . . . 18 $/\$
104	103	neneqd 2648	. . . . . . . . . . . . . . . . 17 $/\$
105	102, 104	syl 17	. . . . . . . . . . . . . . . 16 $/\$
106	105	adantl 473	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
107		pm2.53 380	. . . . . . . . . . . . . . 15 $\/$
108	90, 106, 107	sylc 61	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
109	108	ex 441	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
110	109	ralrimiva 2809	. . . . . . . . . . . 12 $/\$ $/\$
111	110	ralrimiva 2809	. . . . . . . . . . 11 $/\$
112	111	adantr 472	. . . . . . . . . 10 $/\$ $/\$
113	61, 112	jca 541	. . . . . . . . 9 $/\$ $/\$ $/\$
114		reu2 3214	. . . . . . . . 9 $/\$ $/\$
115	113, 114	sylibr 217	. . . . . . . 8 $/\$
116		riotacl2 6283	. . . . . . . 8
117	115, 116	syl 17	. . . . . . 7 $/\$
118		nfriota1 6277	. . . . . . . . . . . 12
119	118	nfcsb1 3364	. . . . . . . . . . . . . 14
120	119, 44	nfin 3630	. . . . . . . . . . . . 13
121	42, 120	nfel 2624	. . . . . . . . . . . 12
122		csbeq1a 3358	. . . . . . . . . . . . . 14
123	122	ineq1d 3624	. . . . . . . . . . . . 13
124	123	eleq2d 2534	. . . . . . . . . . . 12
125	118, 66, 121, 124	elrabf 3182	. . . . . . . . . . 11 $/\$
126	125	biimpi 199	. . . . . . . . . 10 $/\$
127	126	simpld 466	. . . . . . . . 9
128	126	simprd 470	. . . . . . . . . 10
129		ne0i 3728	. . . . . . . . . 10
130	128, 129	syl 17	. . . . . . . . 9
131	127, 130	jca 541	. . . . . . . 8 $/\$
132	120, 71	nfne 2742	. . . . . . . . 9
133	123	neeq1d 2702	. . . . . . . . 9
134	118, 66, 132, 133	elrabf 3182	. . . . . . . 8 $/\$
135	131, 134	sylibr 217	. . . . . . 7
136	117, 135	syl 17	. . . . . 6 $/\$
137	136	ralrimiva 2809	. . . . 5
138	69, 44	nfin 3630	. . . . . . . . . . . . 13
139	138, 71	nfne 2742	. . . . . . . . . . . 12
140		csbeq1a 3358	. . . . . . . . . . . . . 14
141	140	ineq1d 3624	. . . . . . . . . . . . 13
142	141	neeq1d 2702	. . . . . . . . . . . 12
143	21, 66, 139, 142	elrabf 3182	. . . . . . . . . . 11 $/\$
144	143	simprbi 471	. . . . . . . . . 10
145		n0 3732	. . . . . . . . . 10
146	144, 145	sylib 201	. . . . . . . . 9
147	146	adantl 473	. . . . . . . 8 $/\$
148		nfv 1769	. . . . . . . . 9 $/\$
149		simpl 464	. . . . . . . . . 10 $/\$
150	143	simplbi 467	. . . . . . . . . . 11
151	150	adantl 473	. . . . . . . . . 10 $/\$
152		elinel1 3610	. . . . . . . . . . . . . . 15
153	152	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$
154		simplr 770	. . . . . . . . . . . . . . . 16 $/\$ $/\$
155		nfv 1769	. . . . . . . . . . . . . . . . . . 19 $/\$
156		nfcv 2612	. . . . . . . . . . . . . . . . . . . 20
157	69, 156	nfel 2624	. . . . . . . . . . . . . . . . . . 19
158	155, 157	nfim 2023	. . . . . . . . . . . . . . . . . 18 $/\$
159		eleq1 2537	. . . . . . . . . . . . . . . . . . . 20
160	159	anbi2d 718	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
161	140	eleq1d 2533	. . . . . . . . . . . . . . . . . . 19
162	160, 161	imbi12d 327	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
163		disjinfi.b	. . . . . . . . . . . . . . . . . 18 $/\$
164	158, 162, 163	chvar 2119	. . . . . . . . . . . . . . . . 17 $/\$
165	164	adantr 472	. . . . . . . . . . . . . . . 16 $/\$ $/\$
166		eqid 2471	. . . . . . . . . . . . . . . . 17
167	166	elrnmpt1 5089	. . . . . . . . . . . . . . . 16 $/\$
168	154, 165, 167	syl2anc 673	. . . . . . . . . . . . . . 15 $/\$ $/\$
169		nfcv 2612	. . . . . . . . . . . . . . . . 17
170	140	equcoms 1872	. . . . . . . . . . . . . . . . . 18
171	170	eqcomd 2477	. . . . . . . . . . . . . . . . 17
172	69, 169, 171	cbvmpt 4487	. . . . . . . . . . . . . . . 16
173	172	rneqi 5067	. . . . . . . . . . . . . . 15
174	168, 173	syl6eleq 2559	. . . . . . . . . . . . . 14 $/\$ $/\$
175		elunii 4195	. . . . . . . . . . . . . 14 $/\$
176	153, 174, 175	syl2anc 673	. . . . . . . . . . . . 13 $/\$ $/\$
177		elinel2 3611	. . . . . . . . . . . . . 14
178	177	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$
179	176, 178	elind 3609	. . . . . . . . . . . 12 $/\$ $/\$
180		nfv 1769	. . . . . . . . . . . . . . 15
181	42, 138	nfel 2624	. . . . . . . . . . . . . . 15
182	141	eleq2d 2534	. . . . . . . . . . . . . . 15
183	180, 181, 182	cbvriota 6280	. . . . . . . . . . . . . 14
184	183	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
185		simpr 468	. . . . . . . . . . . . . . 15 $/\$ $/\$
186	154, 185	jca 541	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
187		rspe 2844	. . . . . . . . . . . . . . . . . 18 $/\$
188	187	adantll 728	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
189		simpll 768	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
190		sbequ 2225	. . . . . . . . . . . . . . . . . . . . . . . . 25
191		sbsbc 3259	. . . . . . . . . . . . . . . . . . . . . . . . . 26
192	191	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
193		sbcel2 3782	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
194		csbin 3803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
195		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
196		csbconstg 3362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
197	195, 196	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
198	197	ineq2i 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
199	194, 198	eqtri 2493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
200	199	eleq2i 2541	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
201	193, 200	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . 26
202	201	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25
203	190, 192, 202	3bitrd 287	. . . . . . . . . . . . . . . . . . . . . . . 24
204	203	anbi2d 718	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
205		eqeq2 2482	. . . . . . . . . . . . . . . . . . . . . . 23
206	204, 205	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
207	206	cbvralv 3005	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
208	207	ralbii 2823	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
209		nfv 1769	. . . . . . . . . . . . . . . . . . . . 21 $/\$
210	68, 44	nfin 3630	. . . . . . . . . . . . . . . . . . . . . . . . 25
211	42, 210	nfel 2624	. . . . . . . . . . . . . . . . . . . . . . . 24
212	181, 211	nfan 2031	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
213		nfv 1769	. . . . . . . . . . . . . . . . . . . . . . 23
214	212, 213	nfim 2023	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
215	66, 214	nfral 2789	. . . . . . . . . . . . . . . . . . . . 21 $/\$
216	182	anbi1d 719	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
217		eqeq1 2475	. . . . . . . . . . . . . . . . . . . . . . 23
218	216, 217	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
219	218	ralbidv 2829	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
220	209, 215, 219	cbvral 3001	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
221		biid 244	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
222		sbsbc 3259	. . . . . . . . . . . . . . . . . . . . . . . . . 26
223		sbcel2 3782	. . . . . . . . . . . . . . . . . . . . . . . . . 26
224		csbin 3803	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
225		csbco 3359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
226		csbconstg 3362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
227	195, 226	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
228	225, 227	ineq12i 3623	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
229		eqid 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
230	224, 228, 229	3eqtri 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
231	230	eleq2i 2541	. . . . . . . . . . . . . . . . . . . . . . . . . 26
232	222, 223, 231	3bitrri 280	. . . . . . . . . . . . . . . . . . . . . . . . 25
233	232	anbi2i 708	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
234	233	imbi1i 332	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
235	234	ralbii 2823	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
236	235	ralbii 2823	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
237	221, 236	bitri 257	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
238	208, 220, 237	3bitri 279	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
239	112, 238	sylib 201	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
240	189, 179, 239	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
241	188, 240	jca 541	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
242		reu2 3214	. . . . . . . . . . . . . . . 16 $/\$ $/\$
243	241, 242	sylibr 217	. . . . . . . . . . . . . . 15 $/\$ $/\$
244		riota1 6288	. . . . . . . . . . . . . . 15 $/\$
245	243, 244	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
246	186, 245	mpbid 215	. . . . . . . . . . . . 13 $/\$ $/\$
247	184, 246	eqtr2d 2506	. . . . . . . . . . . 12 $/\$ $/\$
248	179, 247	jca 541	. . . . . . . . . . 11 $/\$ $/\$ $/\$
249	248	ex 441	. . . . . . . . . 10 $/\$ $/\$
250	149, 151, 249	syl2anc 673	. . . . . . . . 9 $/\$ $/\$
251	148, 250	eximd 1980	. . . . . . . 8 $/\$ $/\$
252	147, 251	mpd 15	. . . . . . 7 $/\$ $/\$
253		df-rex 2762	. . . . . . 7 $/\$
254	252, 253	sylibr 217	. . . . . 6 $/\$
255	254	ralrimiva 2809	. . . . 5
256	137, 255	jca 541	. . . 4 $/\$
257		eqid 2471	. . . . 5
258	257	fompt 37538	. . . 4 $/\$
259	256, 258	sylibr 217	. . 3
260		fodomg 8971	. . 3
261	11, 259, 260	sylc 61	. 2
262		domfi 7811	. 2 $/\$
263	7, 261, 262	syl2anc 673	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1452

wex 1671

wsb 1805

wcel 1904

wne 2641

wral 2756

wrex 2757

wreu 2758

crab 2760

cvv 3031

wsbc 3255

csb 3349

cin 3389

wss 3390

c0 3722

cuni 4190 Disj wdisj 4366 class class class wbr 4395

cmpt 4454

crn 4840

wfo 5587

crio 6269

cdom 7585

cfn 7587

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-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-ac2 8911

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 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-rmo 2764 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-disj 4367 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-se 4799 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-isom 5598 df-riota 6270 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-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-fin 7591 df-card 8391 df-acn 8394 df-ac 8565

This theorem is referenced by: fsumiunss 37750 sge0iunmptlemre 38371

W3C validator