dffi3 - Metamath Proof Explorer

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

Theorem dffi3 7677

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 7669	. . . 4 $/\$
2		fr0g 6887	. . . . . . . 8
3		frfnom 6886	. . . . . . . . 9
4		peano1 6494	. . . . . . . . 9
5		fnfvelrn 5837	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 667	. . . . . . . 8
7	2, 6	syl6eqelr 2530	. . . . . . 7
8		elssuni 4118	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10		reeanv 2886	. . . . . . . . 9 $/\$ $/\$
11		eliun 4172	. . . . . . . . . 10
12		eliun 4172	. . . . . . . . . 10
13	11, 12	anbi12i 692	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 5961	. . . . . . . . . . . 12
15	14	eleq2d 2508	. . . . . . . . . . 11
16		fniunfv 5961	. . . . . . . . . . . 12
17	16	eleq2d 2508	. . . . . . . . . . 11
18	15, 17	anbi12d 705	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 273	. . . . . . . 8 $/\$ $/\$
21		ordom 6484	. . . . . . . . . . . . . . . 16
22		ordunel 6437	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1296	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 463	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 750	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 529	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6481	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6481	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 721	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 4756	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 656	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3778	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 504	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3380	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3380	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3381	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 2923	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 705	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3380	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3381	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 2923	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 705	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7665	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3387	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3556	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3567	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 3863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 6863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 6889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 4721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 2919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3387	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 600	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6503	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 430	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 460	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2812	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 434	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 462	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5688	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3405	. . . . . . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2797	. . . . . . . . . . . . . 14
149	148	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3516	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3375	. . . . . . . . . . . . . . 15
153		fveq2 5688	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3381	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 320	. . . . . . . . . . . . . 14
156		sseq1 3374	. . . . . . . . . . . . . . 15
157		fveq2 5688	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3380	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 320	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3076	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3352	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 751	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 529	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3517	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3374	. . . . . . . . . . . . . . 15
168	109	sseq1d 3380	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 320	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3076	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3352	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 721	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6495	. . . . . . . . . . . . . . 15
175		fveq2 5688	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4211	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 20	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 750	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 751	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2442	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3542	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2452	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3543	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2452	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3078	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1213	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 2973	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4430	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2447	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2756	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3103	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 212	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2441	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6199	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2532	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5698	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6375	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4472	. . . . . . . . . . . . . . . . 17
199		elssuni 4118	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3364	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 3863	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 462	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2780	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6640	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 208	. . . . . . . . . . . . . . . . . 18
207		frn 5562	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4434	. . . . . . . . . . . . . . . 16
210		nfcv 2577	. . . . . . . . . . . . . . . . 17
211		nfcv 2577	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6145	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 640	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5063	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 6889	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 657	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2518	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3354	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 5961	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2531	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 434	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 480	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2846	. . . . . . . . 9 $/\$
225	224	imp 429	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 473	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2806	. . . . . 6
228	136	simpld 456	. . . . . . . . . . . 12 $/\$
229		fvex 5698	. . . . . . . . . . . . 13
230	229	elpw2 4453	. . . . . . . . . . . 12
231	228, 230	sylibr 212	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2797	. . . . . . . . . 10
233		fnfvrnss 5868	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 658	. . . . . . . . 9
235		sspwuni 4253	. . . . . . . . 9
236	234, 235	sylib 196	. . . . . . . 8
237		ssexg 4435	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 657	. . . . . . 7
239		sseq2 3375	. . . . . . . . 9
240		eleq2 2502	. . . . . . . . . . 11
241	240	raleqbi1dv 2923	. . . . . . . . . 10
242	241	raleqbi1dv 2923	. . . . . . . . 9
243	239, 242	anbi12d 705	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3104	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 16	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 908	. . . . 5 $/\$
247		intss1 4140	. . . . 5 $/\$ $/\$
248	246, 247	syl 16	. . . 4 $/\$
249	1, 248	eqsstrd 3387	. . 3
250	249, 236	eqssd 3370	. 2
251		df-ima 4849	. . 3
252	251	unieqi 4097	. 2
253	250, 252	syl6eqr 2491	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1364

wcel 1761

cab 2427

wral 2713

wrex 2714

cvv 2970

cun 3323

cin 3324

wss 3325

c0 3634

cpw 3857

csn 3874

cuni 4088

cint 4125

ciun 4168

cmpt 4347

word 4714

con0 4715

csuc 4717

cxp 4834

crn 4837

cres 4838

cima 4839

wfn 5410

wf 5411

cfv 5415

cmpt2 6092

com 6475

crdg 6861

cfi 7656

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-reu 2720 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-oadd 6920 df-er 7097 df-en 7307 df-fin 7310 df-fi 7657

This theorem is referenced by: (None)

W3C validator