dffi3 - Metamath Proof Explorer

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

Theorem dffi3 7681

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 7673	. . . 4 $/\$
2		fr0g 6891	. . . . . . . 8
3		frfnom 6890	. . . . . . . . 9
4		peano1 6495	. . . . . . . . 9
5		fnfvelrn 5840	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 672	. . . . . . . 8
7	2, 6	syl6eqelr 2532	. . . . . . 7
8		elssuni 4121	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10		reeanv 2888	. . . . . . . . 9 $/\$ $/\$
11		eliun 4175	. . . . . . . . . 10
12		eliun 4175	. . . . . . . . . 10
13	11, 12	anbi12i 697	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 5964	. . . . . . . . . . . 12
15	14	eleq2d 2510	. . . . . . . . . . 11
16		fniunfv 5964	. . . . . . . . . . . 12
17	16	eleq2d 2510	. . . . . . . . . . 11
18	15, 17	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 273	. . . . . . . 8 $/\$ $/\$
21		ordom 6485	. . . . . . . . . . . . . . . 16
22		ordunel 6438	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1301	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 755	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6482	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6482	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 4760	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3781	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 507	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3383	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3383	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3384	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 2925	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3383	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3384	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 2925	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7669	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3390	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3559	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2550	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6376	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4121	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3367	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 2975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 3866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6166	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 6867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3363	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 2975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 4725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 2921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3390	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 543	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6504	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 430	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2814	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 434	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5691	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3408	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	syl 16	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
145	140, 144	jaod 380	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
146	32, 145	sylbid 215	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	146	ralrimiva 2799	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2799	. . . . . . . . . . . . . 14
149	148	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3519	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3378	. . . . . . . . . . . . . . 15
153		fveq2 5691	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3384	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 320	. . . . . . . . . . . . . 14
156		sseq1 3377	. . . . . . . . . . . . . . 15
157		fveq2 5691	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3383	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 320	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3079	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3355	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 756	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3520	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3377	. . . . . . . . . . . . . . 15
168	109	sseq1d 3383	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 320	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3079	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3355	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6496	. . . . . . . . . . . . . . 15
175		fveq2 5691	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4214	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 20	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2444	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3545	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2454	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3546	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2454	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3081	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1218	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 2975	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4433	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2449	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2758	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3106	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 212	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2443	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6200	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2534	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5701	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6376	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4475	. . . . . . . . . . . . . . . . 17
199		elssuni 4121	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3367	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 3866	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2782	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6641	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 208	. . . . . . . . . . . . . . . . . 18
207		frn 5565	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4437	. . . . . . . . . . . . . . . 16
210		nfcv 2579	. . . . . . . . . . . . . . . . 17
211		nfcv 2579	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6146	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 645	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5067	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 6893	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2520	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3357	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 5964	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2533	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 483	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2848	. . . . . . . . 9 $/\$
225	224	imp 429	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 476	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2808	. . . . . 6
228	136	simpld 459	. . . . . . . . . . . 12 $/\$
229		fvex 5701	. . . . . . . . . . . . 13
230	229	elpw2 4456	. . . . . . . . . . . 12
231	228, 230	sylibr 212	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2799	. . . . . . . . . 10
233		fnfvrnss 5871	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 663	. . . . . . . . 9
235		sspwuni 4256	. . . . . . . . 9
236	234, 235	sylib 196	. . . . . . . 8
237		ssexg 4438	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 662	. . . . . . 7
239		sseq2 3378	. . . . . . . . 9
240		eleq2 2504	. . . . . . . . . . 11
241	240	raleqbi1dv 2925	. . . . . . . . . 10
242	241	raleqbi1dv 2925	. . . . . . . . 9
243	239, 242	anbi12d 710	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3107	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 16	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 913	. . . . 5 $/\$
247		intss1 4143	. . . . 5 $/\$ $/\$
248	246, 247	syl 16	. . . 4 $/\$
249	1, 248	eqsstrd 3390	. . 3
250	249, 236	eqssd 3373	. 2
251		df-ima 4853	. . 3
252	251	unieqi 4100	. 2
253	250, 252	syl6eqr 2493	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1369

wcel 1756

cab 2429

wral 2715

wrex 2716

cvv 2972

cun 3326

cin 3327

wss 3328

c0 3637

cpw 3860

csn 3877

cuni 4091

cint 4128

ciun 4171

cmpt 4350

word 4718

con0 4719

csuc 4721

cxp 4838

crn 4841

cres 4842

cima 4843

wfn 5413

wf 5414

cfv 5418

cmpt2 6093

com 6476

crdg 6865

cfi 7660

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-reu 2722 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-pss 3344 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-tp 3882 df-op 3884 df-uni 4092 df-int 4129 df-iun 4173 df-br 4293 df-opab 4351 df-mpt 4352 df-tr 4386 df-eprel 4632 df-id 4636 df-po 4641 df-so 4642 df-fr 4679 df-we 4681 df-ord 4722 df-on 4723 df-lim 4724 df-suc 4725 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-om 6477 df-1st 6577 df-2nd 6578 df-recs 6832 df-rdg 6866 df-1o 6920 df-oadd 6924 df-er 7101 df-en 7311 df-fin 7314 df-fi 7661

This theorem is referenced by: (None)

W3C validator