dffi3 - Metamath Proof Explorer

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

Theorem dffi3 8337

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 8329	. . . 4 $/\$
2		fr0g 7531	. . . . . . . 8
3		frfnom 7530	. . . . . . . . 9
4		peano1 7085	. . . . . . . . 9
5		fnfvelrn 6356	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 708	. . . . . . . 8
7	2, 6	syl6eqelr 2710	. . . . . . 7
8		elssuni 4467	. . . . . . 7
9	7, 8	syl 17	. . . . . 6
10		reeanv 3107	. . . . . . . . 9 $/\$ $/\$
11		eliun 4524	. . . . . . . . . 10
12		eliun 4524	. . . . . . . . . 10
13	11, 12	anbi12i 733	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 6505	. . . . . . . . . . . 12
15	14	eleq2d 2687	. . . . . . . . . . 11
16		fniunfv 6505	. . . . . . . . . . . 12
17	16	eleq2d 2687	. . . . . . . . . . 11
18	15, 17	anbi12d 747	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 288	. . . . . . . 8 $/\$ $/\$
21		ordom 7074	. . . . . . . . . . . . . . . 16
22		ordunel 7027	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1411	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 794	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 7071	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 7071	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 763	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 5765	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 4073	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 270	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 3146	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 3146	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 8325	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3639	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 4164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 7237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 7507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 7533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3610	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 4222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 567	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 5729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 3142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 242	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 8328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 7237	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3639	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 566	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 629	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 7094	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 446	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 479	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2932	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 450	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3657	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
145	140, 144	jaod 395	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
146	32, 145	sylbid 230	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	146	ralrimiva 2966	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2966	. . . . . . . . . . . . . 14
149	148	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3776	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3627	. . . . . . . . . . . . . . 15
153		fveq2 6191	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3633	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 334	. . . . . . . . . . . . . 14
156		sseq1 3626	. . . . . . . . . . . . . . 15
157		fveq2 6191	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3632	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 334	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3322	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 66	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3602	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 796	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 554	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3777	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3626	. . . . . . . . . . . . . . 15
168	109	sseq1d 3632	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 334	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3322	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 66	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3602	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 763	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 7086	. . . . . . . . . . . . . . 15
175		fveq2 6191	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4564	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 18	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 794	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 796	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2623	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3807	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2632	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3808	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2632	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3324	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1326	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 3203	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4799	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2626	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 3057	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3350	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 224	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2622	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6770	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2712	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 6201	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6953	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4848	. . . . . . . . . . . . . . . . 17
199		elssuni 4467	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3614	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 4164	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 224	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2977	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 7237	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 220	. . . . . . . . . . . . . . . . . 18
207		frn 6053	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4803	. . . . . . . . . . . . . . . 16
210		nfcv 2764	. . . . . . . . . . . . . . . . 17
211		nfcv 2764	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6715	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 677	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5353	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 7533	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 694	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2704	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3604	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 6505	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2711	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 450	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 500	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 3038	. . . . . . . . 9 $/\$
225	224	imp 445	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 493	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2971	. . . . . 6
228	136	simpld 475	. . . . . . . . . . . 12 $/\$
229		fvex 6201	. . . . . . . . . . . . 13
230	229	elpw2 4828	. . . . . . . . . . . 12
231	228, 230	sylibr 224	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2966	. . . . . . . . . 10
233		fnfvrnss 6390	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 695	. . . . . . . . 9
235		sspwuni 4611	. . . . . . . . 9
236	234, 235	sylib 208	. . . . . . . 8
237		ssexg 4804	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 694	. . . . . . 7
239		sseq2 3627	. . . . . . . . 9
240		eleq2 2690	. . . . . . . . . . 11
241	240	raleqbi1dv 3146	. . . . . . . . . 10
242	241	raleqbi1dv 3146	. . . . . . . . 9
243	239, 242	anbi12d 747	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3351	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 17	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 957	. . . . 5 $/\$
247		intss1 4492	. . . . 5 $/\$ $/\$
248	246, 247	syl 17	. . . 4 $/\$
249	1, 248	eqsstrd 3639	. . 3
250	249, 236	eqssd 3620	. 2
251		df-ima 5127	. . 3
252	251	unieqi 4445	. 2
253	250, 252	syl6eqr 2674	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990

cab 2608

wral 2912

wrex 2913

cvv 3200

cun 3572

cin 3573

wss 3574

c0 3915

cpw 4158

csn 4177

cuni 4436

cint 4475

ciun 4520

cmpt 4729

cxp 5112

crn 5115

cres 5116

cima 5117

word 5722

con0 5723

csuc 5725

wfn 5883

wf 5884

cfv 5888

cmpt2 6652

com 7065

crdg 7505

cfi 8316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-fin 7959 df-fi 8317

This theorem is referenced by: (None)

W3C validator