dffi3 - Metamath Proof Explorer

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

Theorem dffi3 7891

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 7883	. . . 4 $/\$
2		fr0g 7101	. . . . . . . 8
3		frfnom 7100	. . . . . . . . 9
4		peano1 6703	. . . . . . . . 9
5		fnfvelrn 6018	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 672	. . . . . . . 8
7	2, 6	syl6eqelr 2564	. . . . . . 7
8		elssuni 4275	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10		reeanv 3029	. . . . . . . . 9 $/\$ $/\$
11		eliun 4330	. . . . . . . . . 10
12		eliun 4330	. . . . . . . . . 10
13	11, 12	anbi12i 697	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 6147	. . . . . . . . . . . 12
15	14	eleq2d 2537	. . . . . . . . . . 11
16		fniunfv 6147	. . . . . . . . . . . 12
17	16	eleq2d 2537	. . . . . . . . . . 11
18	15, 17	anbi12d 710	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 273	. . . . . . . 8 $/\$ $/\$
21		ordom 6693	. . . . . . . . . . . . . . . 16
22		ordunel 6646	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1311	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 466	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 755	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6690	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6690	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 4919	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 661	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3929	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 507	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3531	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3531	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3532	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 3066	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3531	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3532	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 3066	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 710	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7879	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3538	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3225	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 4016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 7077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 7103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3511	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 4066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 544	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 4884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 3062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3538	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 543	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 603	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6712	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 430	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 463	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2833	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 434	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 465	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5866	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3556	. . . . . . . . . . . . . . . . . . . 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 2878	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2878	. . . . . . . . . . . . . 14
149	148	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3667	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3526	. . . . . . . . . . . . . . 15
153		fveq2 5866	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3532	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 320	. . . . . . . . . . . . . 14
156		sseq1 3525	. . . . . . . . . . . . . . 15
157		fveq2 5866	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3531	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 320	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3223	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3503	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 756	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3668	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3525	. . . . . . . . . . . . . . 15
168	109	sseq1d 3531	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 320	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3223	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3503	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6704	. . . . . . . . . . . . . . 15
175		fveq2 5866	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4369	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 20	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3693	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3694	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3225	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1228	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 3116	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4588	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2471	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2980	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3250	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 212	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2467	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6396	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2566	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5876	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6580	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4630	. . . . . . . . . . . . . . . . 17
199		elssuni 4275	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3515	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 4016	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2891	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6851	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 208	. . . . . . . . . . . . . . . . . 18
207		frn 5737	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4592	. . . . . . . . . . . . . . . 16
210		nfcv 2629	. . . . . . . . . . . . . . . . 17
211		nfcv 2629	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6341	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 645	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5230	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 7103	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 662	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2558	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 6147	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2565	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 483	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2962	. . . . . . . . 9 $/\$
225	224	imp 429	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 476	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2885	. . . . . 6
228	136	simpld 459	. . . . . . . . . . . 12 $/\$
229		fvex 5876	. . . . . . . . . . . . 13
230	229	elpw2 4611	. . . . . . . . . . . 12
231	228, 230	sylibr 212	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2878	. . . . . . . . . 10
233		fnfvrnss 6049	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 663	. . . . . . . . 9
235		sspwuni 4411	. . . . . . . . 9
236	234, 235	sylib 196	. . . . . . . 8
237		ssexg 4593	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 662	. . . . . . 7
239		sseq2 3526	. . . . . . . . 9
240		eleq2 2540	. . . . . . . . . . 11
241	240	raleqbi1dv 3066	. . . . . . . . . 10
242	241	raleqbi1dv 3066	. . . . . . . . 9
243	239, 242	anbi12d 710	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3251	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 16	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 920	. . . . 5 $/\$
247		intss1 4297	. . . . 5 $/\$ $/\$
248	246, 247	syl 16	. . . 4 $/\$
249	1, 248	eqsstrd 3538	. . 3
250	249, 236	eqssd 3521	. 2
251		df-ima 5012	. . 3
252	251	unieqi 4254	. 2
253	250, 252	syl6eqr 2526	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1379

wcel 1767

cab 2452

wral 2814

wrex 2815

cvv 3113

cun 3474

cin 3475

wss 3476

c0 3785

cpw 4010

csn 4027

cuni 4245

cint 4282

ciun 4325

cmpt 4505

word 4877

con0 4878

csuc 4880

cxp 4997

crn 5000

cres 5001

cima 5002

wfn 5583

wf 5584

cfv 5588

cmpt2 6286

com 6684

crdg 7075

cfi 7870

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-1o 7130 df-oadd 7134 df-er 7311 df-en 7517 df-fin 7520 df-fi 7871

This theorem is referenced by: (None)

W3C validator