dffi3 - Metamath Proof Explorer

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

Theorem dffi3 7893

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 7885	. . . 4 $/\$
2		fr0g 7103	. . . . . . . 8
3		frfnom 7102	. . . . . . . . 9
4		peano1 6704	. . . . . . . . 9
5		fnfvelrn 6013	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 672	. . . . . . . 8
7	2, 6	syl6eqelr 2540	. . . . . . 7
8		elssuni 4264	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10		reeanv 3011	. . . . . . . . 9 $/\$ $/\$
11		eliun 4320	. . . . . . . . . 10
12		eliun 4320	. . . . . . . . . 10
13	11, 12	anbi12i 697	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 6144	. . . . . . . . . . . 12
15	14	eleq2d 2513	. . . . . . . . . . 11
16		fniunfv 6144	. . . . . . . . . . . 12
17	16	eleq2d 2513	. . . . . . . . . . 11
18	15, 17	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 273	. . . . . . . 8 $/\$ $/\$
21		ordom 6694	. . . . . . . . . . . . . . . 16
22		ordunel 6647	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1312	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 756	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6691	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6691	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 4909	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3916	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 507	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3516	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3516	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3517	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 3048	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3516	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3517	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 3048	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7881	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3523	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 4003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4528	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 7079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 7105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 4053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 3044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3523	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 543	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6713	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 430	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2812	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 434	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5856	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3541	. . . . . . . . . . . . . . . . . . . 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 2857	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2857	. . . . . . . . . . . . . 14
149	148	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3652	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3511	. . . . . . . . . . . . . . 15
153		fveq2 5856	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3517	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 320	. . . . . . . . . . . . . 14
156		sseq1 3510	. . . . . . . . . . . . . . 15
157		fveq2 5856	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3516	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 320	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3205	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3488	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 757	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3653	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3510	. . . . . . . . . . . . . . 15
168	109	sseq1d 3516	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 320	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3205	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3488	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6705	. . . . . . . . . . . . . . 15
175		fveq2 5856	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4359	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 20	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 757	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2444	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3678	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2457	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3679	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2457	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3207	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1229	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 3098	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4578	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2447	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2961	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3232	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 212	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2443	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6397	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2542	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5866	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6581	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4620	. . . . . . . . . . . . . . . . 17
199		elssuni 4264	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3500	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 4003	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2870	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6852	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 208	. . . . . . . . . . . . . . . . . 18
207		frn 5727	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4582	. . . . . . . . . . . . . . . 16
210		nfcv 2605	. . . . . . . . . . . . . . . . 17
211		nfcv 2605	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6342	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 645	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5220	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 7105	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2534	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3490	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 6144	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2541	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 483	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2942	. . . . . . . . 9 $/\$
225	224	imp 429	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 476	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2864	. . . . . 6
228	136	simpld 459	. . . . . . . . . . . 12 $/\$
229		fvex 5866	. . . . . . . . . . . . 13
230	229	elpw2 4601	. . . . . . . . . . . 12
231	228, 230	sylibr 212	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2857	. . . . . . . . . 10
233		fnfvrnss 6044	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 663	. . . . . . . . 9
235		sspwuni 4401	. . . . . . . . 9
236	234, 235	sylib 196	. . . . . . . 8
237		ssexg 4583	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 662	. . . . . . 7
239		sseq2 3511	. . . . . . . . 9
240		eleq2 2516	. . . . . . . . . . 11
241	240	raleqbi1dv 3048	. . . . . . . . . 10
242	241	raleqbi1dv 3048	. . . . . . . . 9
243	239, 242	anbi12d 710	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3233	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 16	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 922	. . . . 5 $/\$
247		intss1 4286	. . . . 5 $/\$ $/\$
248	246, 247	syl 16	. . . 4 $/\$
249	1, 248	eqsstrd 3523	. . 3
250	249, 236	eqssd 3506	. 2
251		df-ima 5002	. . 3
252	251	unieqi 4243	. 2
253	250, 252	syl6eqr 2502	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1383

wcel 1804

cab 2428

wral 2793

wrex 2794

cvv 3095

cun 3459

cin 3460

wss 3461

c0 3770

cpw 3997

csn 4014

cuni 4234

cint 4271

ciun 4315

cmpt 4495

word 4867

con0 4868

csuc 4870

cxp 4987

crn 4990

cres 4991

cima 4992

wfn 5573

wf 5574

cfv 5578

cmpt2 6283

com 6685

crdg 7077

cfi 7872

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-ral 2798 df-rex 2799 df-reu 2800 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-oadd 7136 df-er 7313 df-en 7519 df-fin 7522 df-fi 7873

This theorem is referenced by: (None)

W3C validator