dffi3 - Metamath Proof Explorer

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

Theorem dffi3 7806

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 7798	. . . 4 $/\$
2		fr0g 7019	. . . . . . . 8
3		frfnom 7018	. . . . . . . . 9
4		peano1 6618	. . . . . . . . 9
5		fnfvelrn 5930	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 670	. . . . . . . 8
7	2, 6	syl6eqelr 2479	. . . . . . 7
8		elssuni 4192	. . . . . . 7
9	7, 8	syl 16	. . . . . 6
10		reeanv 2950	. . . . . . . . 9 $/\$ $/\$
11		eliun 4248	. . . . . . . . . 10
12		eliun 4248	. . . . . . . . . 10
13	11, 12	anbi12i 695	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 6060	. . . . . . . . . . . 12
15	14	eleq2d 2452	. . . . . . . . . . 11
16		fniunfv 6060	. . . . . . . . . . . 12
17	16	eleq2d 2452	. . . . . . . . . . 11
18	15, 17	anbi12d 708	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 273	. . . . . . . 8 $/\$ $/\$
21		ordom 6608	. . . . . . . . . . . . . . . 16
22		ordunel 6561	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1309	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 464	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 754	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 530	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6605	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 464	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6605	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 724	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 4833	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3847	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 505	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3444	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 255	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3444	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3445	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 2987	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3444	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3445	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 2987	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 708	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7794	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3451	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3621	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2509	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4192	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 3933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 6995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 7021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 660	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 542	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 4798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 2983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 227	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 541	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 601	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6627	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 428	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 461	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 432	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 463	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5774	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3469	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	syl 16	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
145	140, 144	jaod 378	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
146	32, 145	sylbid 215	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	146	ralrimiva 2796	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2796	. . . . . . . . . . . . . 14
149	148	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3581	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3439	. . . . . . . . . . . . . . 15
153		fveq2 5774	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3445	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 318	. . . . . . . . . . . . . 14
156		sseq1 3438	. . . . . . . . . . . . . . 15
157		fveq2 5774	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3444	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 318	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3144	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3416	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 755	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 530	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3582	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3438	. . . . . . . . . . . . . . 15
168	109	sseq1d 3444	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 318	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3144	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 61	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3416	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6619	. . . . . . . . . . . . . . 15
175		fveq2 5774	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4287	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 20	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 754	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2383	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3607	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2396	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3608	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2396	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3146	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1226	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 3037	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4506	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2386	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2900	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3171	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 212	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2382	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6311	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5784	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6495	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4548	. . . . . . . . . . . . . . . . 17
199		elssuni 4192	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3428	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 3933	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 212	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2809	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6766	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 208	. . . . . . . . . . . . . . . . . 18
207		frn 5645	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4510	. . . . . . . . . . . . . . . 16
210		nfcv 2544	. . . . . . . . . . . . . . . . 17
211		nfcv 2544	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6256	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 643	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5143	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 7021	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 660	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2473	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3418	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 6060	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2480	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 432	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 481	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2881	. . . . . . . . 9 $/\$
225	224	imp 427	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 474	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2803	. . . . . 6
228	136	simpld 457	. . . . . . . . . . . 12 $/\$
229		fvex 5784	. . . . . . . . . . . . 13
230	229	elpw2 4529	. . . . . . . . . . . 12
231	228, 230	sylibr 212	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2796	. . . . . . . . . 10
233		fnfvrnss 5961	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 661	. . . . . . . . 9
235		sspwuni 4332	. . . . . . . . 9
236	234, 235	sylib 196	. . . . . . . 8
237		ssexg 4511	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 660	. . . . . . 7
239		sseq2 3439	. . . . . . . . 9
240		eleq2 2455	. . . . . . . . . . 11
241	240	raleqbi1dv 2987	. . . . . . . . . 10
242	241	raleqbi1dv 2987	. . . . . . . . 9
243	239, 242	anbi12d 708	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3172	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 16	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 920	. . . . 5 $/\$
247		intss1 4214	. . . . 5 $/\$ $/\$
248	246, 247	syl 16	. . . 4 $/\$
249	1, 248	eqsstrd 3451	. . 3
250	249, 236	eqssd 3434	. 2
251		df-ima 4926	. . 3
252	251	unieqi 4172	. 2
253	250, 252	syl6eqr 2441	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wceq 1399

wcel 1826

cab 2367

wral 2732

wrex 2733

cvv 3034

cun 3387

cin 3388

wss 3389

c0 3711

cpw 3927

csn 3944

cuni 4163

cint 4199

ciun 4243

cmpt 4425

word 4791

con0 4792

csuc 4794

cxp 4911

crn 4914

cres 4915

cima 4916

wfn 5491

wf 5492

cfv 5496

cmpt2 6198

com 6599

crdg 6993

cfi 7785

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-reu 2739 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-1st 6699 df-2nd 6700 df-recs 6960 df-rdg 6994 df-1o 7048 df-oadd 7052 df-er 7229 df-en 7436 df-fin 7439 df-fi 7786

This theorem is referenced by: (None)

W3C validator