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 7945

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 7937	. . . 4 $/\$
2		fr0g 7153	. . . . . . . 8
3		frfnom 7152	. . . . . . . . 9
4		peano1 6712	. . . . . . . . 9
5		fnfvelrn 6019	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 678	. . . . . . . 8
7	2, 6	syl6eqelr 2538	. . . . . . 7
8		elssuni 4227	. . . . . . 7
9	7, 8	syl 17	. . . . . 6
10		reeanv 2958	. . . . . . . . 9 $/\$ $/\$
11		eliun 4283	. . . . . . . . . 10
12		eliun 4283	. . . . . . . . . 10
13	11, 12	anbi12i 703	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 6152	. . . . . . . . . . . 12
15	14	eleq2d 2514	. . . . . . . . . . 11
16		fniunfv 6152	. . . . . . . . . . . 12
17	16	eleq2d 2514	. . . . . . . . . . 11
18	15, 17	anbi12d 717	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 277	. . . . . . . 8 $/\$ $/\$
21		ordom 6701	. . . . . . . . . . . . . . . 16
22		ordunel 6654	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1351	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 468	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 764	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 535	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6698	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 468	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6698	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 733	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 5464	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 667	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3871	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 510	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3459	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 259	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3459	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3460	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 2995	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3459	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3460	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 2995	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 717	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7933	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3466	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3161	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4227	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4544	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 3957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 7129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6351	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 7155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 3048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 4010	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 5429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 2991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 546	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 608	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6721	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 432	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 465	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2757	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 436	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5865	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3484	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
145	140, 144	jaod 382	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
146	32, 145	sylbid 219	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	146	ralrimiva 2802	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2802	. . . . . . . . . . . . . 14
149	148	adantr 467	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3597	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3454	. . . . . . . . . . . . . . 15
153		fveq2 5865	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3460	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 322	. . . . . . . . . . . . . 14
156		sseq1 3453	. . . . . . . . . . . . . . 15
157		fveq2 5865	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3459	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 322	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3159	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 63	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3431	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 766	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 535	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3598	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3453	. . . . . . . . . . . . . . 15
168	109	sseq1d 3459	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 322	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3159	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 63	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3431	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 733	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6713	. . . . . . . . . . . . . . 15
175		fveq2 5865	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4322	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 18	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 764	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2452	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3627	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2461	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3628	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2461	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3161	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1268	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 3048	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4544	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2455	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2908	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3185	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 216	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2451	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6406	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2540	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5875	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6587	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4586	. . . . . . . . . . . . . . . . 17
199		elssuni 4227	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3443	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 3957	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 216	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 467	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2815	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6860	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 212	. . . . . . . . . . . . . . . . . 18
207		frn 5735	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4548	. . . . . . . . . . . . . . . 16
210		nfcv 2592	. . . . . . . . . . . . . . . . 17
211		nfcv 2592	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6351	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 651	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5062	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 7155	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 668	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2532	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3433	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 6152	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2539	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 436	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 486	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2886	. . . . . . . . 9 $/\$
225	224	imp 431	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 479	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2809	. . . . . 6
228	136	simpld 461	. . . . . . . . . . . 12 $/\$
229		fvex 5875	. . . . . . . . . . . . 13
230	229	elpw2 4567	. . . . . . . . . . . 12
231	228, 230	sylibr 216	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2802	. . . . . . . . . 10
233		fnfvrnss 6051	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 669	. . . . . . . . 9
235		sspwuni 4367	. . . . . . . . 9
236	234, 235	sylib 200	. . . . . . . 8
237		ssexg 4549	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 668	. . . . . . 7
239		sseq2 3454	. . . . . . . . 9
240		eleq2 2518	. . . . . . . . . . 11
241	240	raleqbi1dv 2995	. . . . . . . . . 10
242	241	raleqbi1dv 2995	. . . . . . . . 9
243	239, 242	anbi12d 717	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3186	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 17	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 933	. . . . 5 $/\$
247		intss1 4249	. . . . 5 $/\$ $/\$
248	246, 247	syl 17	. . . 4 $/\$
249	1, 248	eqsstrd 3466	. . 3
250	249, 236	eqssd 3449	. 2
251		df-ima 4847	. . 3
252	251	unieqi 4207	. 2
253	250, 252	syl6eqr 2503	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371

wceq 1444

wcel 1887

cab 2437

wral 2737

wrex 2738

cvv 3045

cun 3402

cin 3403

wss 3404

c0 3731

cpw 3951

csn 3968

cuni 4198

cint 4234

ciun 4278

cmpt 4461

cxp 4832

crn 4835

cres 4836

cima 4837

word 5422

con0 5423

csuc 5425

wfn 5577

wf 5578

cfv 5582

cmpt2 6292

com 6692

crdg 7127

cfi 7924

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-fin 7573 df-fi 7925

This theorem is referenced by: (None)

W3C validator