dffi3 - Metamath Proof Explorer

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

Theorem dffi3 7394

Description: The set of finite intersections can be "constructed" inductively by iterating binary intersection

-many times. (Contributed by Mario Carneiro, 21-Mar-2015.)

**Hypothesis**
Ref	Expression
dffi3.1

**Assertion**
Ref	Expression
dffi3

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

Proof of Theorem dffi3 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dffi2 7386	. . . 4 $/\$
2		fr0g 6652	. . . . . . . 8
3		frfnom 6651	. . . . . . . . 9
4		peano1 4823	. . . . . . . . 9
5		fnfvelrn 5826	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 654	. . . . . . . 8
7	2, 6	syl6eqelr 2493	. . . . . . 7
8		elssuni 4003	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10		reeanv 2835	. . . . . . . . 9 $/\$ $/\$
11		eliun 4057	. . . . . . . . . 10
12		eliun 4057	. . . . . . . . . 10
13	11, 12	anbi12i 679	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 5953	. . . . . . . . . . . 12
15	14	eleq2d 2471	. . . . . . . . . . 11
16		fniunfv 5953	. . . . . . . . . . . 12
17	16	eleq2d 2471	. . . . . . . . . . 11
18	15, 17	anbi12d 692	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 8	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 265	. . . . . . . 8 $/\$ $/\$
21		ordom 4813	. . . . . . . . . . . . . . . 16
22		ordunel 4766	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1266	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 453	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 733	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 519	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 4810	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 453	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 4810	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 708	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 4582	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 494	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3335	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 247	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3335	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3336	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 2872	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 692	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3335	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3336	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 2872	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 692	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7382	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3342	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 4664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4304	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 3765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4308	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6111	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 6628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 6654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 28	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 3809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 4547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 528	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 23	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 4832	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 420	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 450	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2764	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 424	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3360	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	syl 16	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
145	140, 144	jaod 370	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
146	32, 145	sylbid 207	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	146	ralrimiva 2749	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2749	. . . . . . . . . . . . . 14
149	148	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3470	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3330	. . . . . . . . . . . . . . 15
153		fveq2 5687	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3336	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 312	. . . . . . . . . . . . . 14
156		sseq1 3329	. . . . . . . . . . . . . . 15
157		fveq2 5687	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3335	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 312	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3018	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 59	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3307	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 734	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 519	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3471	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3329	. . . . . . . . . . . . . . 15
168	109	sseq1d 3335	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 312	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3018	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 59	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3307	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 708	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 4824	. . . . . . . . . . . . . . 15
175		fveq2 5687	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4095	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 19	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 734	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2405	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3495	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2415	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3496	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2415	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3020	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1184	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 2919	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4304	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2410	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2709	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3042	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 204	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2404	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6139	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2495	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5701	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 4664	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4342	. . . . . . . . . . . . . . . . 17
199		elssuni 4003	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3319	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 3765	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 204	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 452	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2732	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6377	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 200	. . . . . . . . . . . . . . . . . 18
207		frn 5556	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 8	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4308	. . . . . . . . . . . . . . . 16
210		nfcv 2540	. . . . . . . . . . . . . . . . 17
211		nfcv 2540	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6093	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 627	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5056	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 6654	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 644	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 5953	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 8	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2494	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 424	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 470	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2797	. . . . . . . . 9 $/\$
225	224	imp 419	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 463	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2758	. . . . . 6
228	136	simpld 446	. . . . . . . . . . . 12 $/\$
229		fvex 5701	. . . . . . . . . . . . 13
230	229	elpw2 4324	. . . . . . . . . . . 12
231	228, 230	sylibr 204	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2749	. . . . . . . . . 10
233		fnfvrnss 5855	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 645	. . . . . . . . 9
235		sspwuni 4136	. . . . . . . . 9
236	234, 235	sylib 189	. . . . . . . 8
237		ssexg 4309	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 644	. . . . . . 7
239		sseq2 3330	. . . . . . . . 9
240		eleq2 2465	. . . . . . . . . . 11
241	240	raleqbi1dv 2872	. . . . . . . . . 10
242	241	raleqbi1dv 2872	. . . . . . . . 9
243	239, 242	anbi12d 692	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3043	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 16	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 889	. . . . 5 $/\$
247		intss1 4025	. . . . 5 $/\$ $/\$
248	246, 247	syl 16	. . . 4 $/\$
249	1, 248	eqsstrd 3342	. . 3
250	249, 236	eqssd 3325	. 2
251		df-ima 4850	. . 3
252	251	unieqi 3985	. 2
253	250, 252	syl6eqr 2454	1

Colors of variables: wff set class

Syntax hints:

wi 4

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

wceq 1649

wcel 1721

cab 2390

wral 2666

wrex 2667

cvv 2916

cun 3278

cin 3279

wss 3280

c0 3588

cpw 3759

csn 3774

cuni 3975

cint 4010

ciun 4053

cmpt 4226

word 4540

con0 4541

csuc 4543

com 4804

cxp 4835

crn 4838

cres 4839

cima 4840

wfn 5408

wf 5409

cfv 5413

cmpt2 6042

crdg 6626

cfi 7373

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-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-oadd 6687 df-er 6864 df-en 7069 df-fin 7072 df-fi 7374

W3C validator