dffi3 - Metamath Proof Explorer

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

Theorem dffi3 7947

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 7939	. . . 4 $/\$
2		fr0g 7157	. . . . . . . 8
3		frfnom 7156	. . . . . . . . 9
4		peano1 6722	. . . . . . . . 9
5		fnfvelrn 6030	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 676	. . . . . . . 8
7	2, 6	syl6eqelr 2519	. . . . . . 7
8		elssuni 4245	. . . . . . 7
9	7, 8	syl 17	. . . . . 6
10		reeanv 2996	. . . . . . . . 9 $/\$ $/\$
11		eliun 4301	. . . . . . . . . 10
12		eliun 4301	. . . . . . . . . 10
13	11, 12	anbi12i 701	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 6163	. . . . . . . . . . . 12
15	14	eleq2d 2492	. . . . . . . . . . 11
16		fniunfv 6163	. . . . . . . . . . . 12
17	16	eleq2d 2492	. . . . . . . . . . 11
18	15, 17	anbi12d 715	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 276	. . . . . . . 8 $/\$ $/\$
21		ordom 6711	. . . . . . . . . . . . . . . 16
22		ordunel 6664	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1347	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 467	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 762	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 534	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6708	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6708	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 731	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 5479	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3899	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 509	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5877	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3491	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 258	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5877	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3491	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3492	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 3033	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5877	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3491	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3492	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 3033	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 715	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7935	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3498	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2549	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 3084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 7133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 7159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 3084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 546	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 5444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 3029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3647	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 230	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 545	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 606	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6731	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 431	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 464	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2794	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 435	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 466	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5877	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3516	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
145	140, 144	jaod 381	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
146	32, 145	sylbid 218	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	146	ralrimiva 2839	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2839	. . . . . . . . . . . . . 14
149	148	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3629	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3486	. . . . . . . . . . . . . . 15
153		fveq2 5877	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3492	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 321	. . . . . . . . . . . . . 14
156		sseq1 3485	. . . . . . . . . . . . . . 15
157		fveq2 5877	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3491	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 321	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3191	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 63	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3463	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 764	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 534	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3630	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3485	. . . . . . . . . . . . . . 15
168	109	sseq1d 3491	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 321	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3191	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 63	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3463	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 731	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6723	. . . . . . . . . . . . . . 15
175		fveq2 5877	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4340	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 18	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 764	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2423	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3657	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2436	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3658	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2436	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3193	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1264	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 3084	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4561	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2426	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2946	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3218	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 215	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2422	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6416	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2521	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5887	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6597	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4603	. . . . . . . . . . . . . . . . 17
199		elssuni 4245	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3475	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 3985	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 215	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 466	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2852	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6870	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 211	. . . . . . . . . . . . . . . . . 18
207		frn 5748	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4565	. . . . . . . . . . . . . . . 16
210		nfcv 2584	. . . . . . . . . . . . . . . . 17
211		nfcv 2584	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6361	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 649	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5077	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 7159	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2513	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 6163	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2520	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 435	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 485	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2924	. . . . . . . . 9 $/\$
225	224	imp 430	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 478	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2846	. . . . . 6
228	136	simpld 460	. . . . . . . . . . . 12 $/\$
229		fvex 5887	. . . . . . . . . . . . 13
230	229	elpw2 4584	. . . . . . . . . . . 12
231	228, 230	sylibr 215	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2839	. . . . . . . . . 10
233		fnfvrnss 6062	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 667	. . . . . . . . 9
235		sspwuni 4385	. . . . . . . . 9
236	234, 235	sylib 199	. . . . . . . 8
237		ssexg 4566	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 666	. . . . . . 7
239		sseq2 3486	. . . . . . . . 9
240		eleq2 2495	. . . . . . . . . . 11
241	240	raleqbi1dv 3033	. . . . . . . . . 10
242	241	raleqbi1dv 3033	. . . . . . . . 9
243	239, 242	anbi12d 715	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3219	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 17	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 930	. . . . 5 $/\$
247		intss1 4267	. . . . 5 $/\$ $/\$
248	246, 247	syl 17	. . . 4 $/\$
249	1, 248	eqsstrd 3498	. . 3
250	249, 236	eqssd 3481	. 2
251		df-ima 4862	. . 3
252	251	unieqi 4225	. 2
253	250, 252	syl6eqr 2481	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370

wceq 1437

wcel 1868

cab 2407

wral 2775

wrex 2776

cvv 3081

cun 3434

cin 3435

wss 3436

c0 3761

cpw 3979

csn 3996

cuni 4216

cint 4252

ciun 4296

cmpt 4479

cxp 4847

crn 4850

cres 4851

cima 4852

word 5437

con0 5438

csuc 5440

wfn 5592

wf 5593

cfv 5597

cmpt2 6303

com 6702

crdg 7131

cfi 7926

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-sep 4543 ax-nul 4551 ax-pow 4598 ax-pr 4656 ax-un 6593

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-ral 2780 df-rex 2781 df-reu 2782 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-int 4253 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4760 df-id 4764 df-po 4770 df-so 4771 df-fr 4808 df-we 4810 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-pred 5395 df-ord 5441 df-on 5442 df-lim 5443 df-suc 5444 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-ov 6304 df-oprab 6305 df-mpt2 6306 df-om 6703 df-1st 6803 df-2nd 6804 df-wrecs 7032 df-recs 7094 df-rdg 7132 df-1o 7186 df-oadd 7190 df-er 7367 df-en 7574 df-fin 7577 df-fi 7927

This theorem is referenced by: (None)

W3C validator