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 7963

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 7955	. . . 4 $/\$
2		fr0g 7171	. . . . . . . 8
3		frfnom 7170	. . . . . . . . 9
4		peano1 6731	. . . . . . . . 9
5		fnfvelrn 6034	. . . . . . . . 9 $/\$
6	3, 4, 5	mp2an 686	. . . . . . . 8
7	2, 6	syl6eqelr 2558	. . . . . . 7
8		elssuni 4219	. . . . . . 7
9	7, 8	syl 17	. . . . . 6
10		reeanv 2944	. . . . . . . . 9 $/\$ $/\$
11		eliun 4274	. . . . . . . . . 10
12		eliun 4274	. . . . . . . . . 10
13	11, 12	anbi12i 711	. . . . . . . . 9 $/\$ $/\$
14		fniunfv 6170	. . . . . . . . . . . 12
15	14	eleq2d 2534	. . . . . . . . . . 11
16		fniunfv 6170	. . . . . . . . . . . 12
17	16	eleq2d 2534	. . . . . . . . . . 11
18	15, 17	anbi12d 725	. . . . . . . . . 10 $/\$ $/\$
19	3, 18	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
20	10, 13, 19	3bitr2i 281	. . . . . . . 8 $/\$ $/\$
21		ordom 6720	. . . . . . . . . . . . . . . 16
22		ordunel 6673	. . . . . . . . . . . . . . . 16 $/\$ $/\$
23	21, 22	mp3an1 1377	. . . . . . . . . . . . . . 15 $/\$
24	23	adantl 473	. . . . . . . . . . . . . 14 $/\$ $/\$
25		simprl 772	. . . . . . . . . . . . . 14 $/\$ $/\$
26	24, 25	jca 541	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
27		nnon 6717	. . . . . . . . . . . . . . . . . . 19
28	27	adantl 473	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		nnon 6717	. . . . . . . . . . . . . . . . . . 19
30	29	ad2antlr 741	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
31		onsseleq 5471	. . . . . . . . . . . . . . . . . 18 $/\$ $\/$
32	28, 30, 31	syl2anc 673	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
33		rzal 3862	. . . . . . . . . . . . . . . . . . . . . . . . . 26
34	33	biantrud 515	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
35		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	35	sseq1d 3445	. . . . . . . . . . . . . . . . . . . . . . . . 25
37	34, 36	bitr3d 263	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
38		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . 26
39	38	sseq1d 3445	. . . . . . . . . . . . . . . . . . . . . . . . 25
40	38	sseq2d 3446	. . . . . . . . . . . . . . . . . . . . . . . . . 26
41	40	raleqbi1dv 2981	. . . . . . . . . . . . . . . . . . . . . . . . 25
42	39, 41	anbi12d 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
43		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . 26
44	43	sseq1d 3445	. . . . . . . . . . . . . . . . . . . . . . . . 25
45	43	sseq2d 3446	. . . . . . . . . . . . . . . . . . . . . . . . . 26
46	45	raleqbi1dv 2981	. . . . . . . . . . . . . . . . . . . . . . . . 25
47	44, 46	anbi12d 725	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
48		ssfii 7951	. . . . . . . . . . . . . . . . . . . . . . . . 25
49	2, 48	eqsstrd 3452	. . . . . . . . . . . . . . . . . . . . . . . 24
50		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
51		eqidd 2472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
52		ineq1 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
53	52	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
54		ineq2 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
55		inidm 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
56	54, 55	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
57	56	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
58	53, 57	rspc2ev 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
59	50, 50, 51, 58	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
60		eqid 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
61	60	rnmpt2 6425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
62	61	abeq2i 2583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
63	59, 62	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	ssriv 3422	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		simpl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
66		fvex 5889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
67	66	uniex 6606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
68	67	pwex 4584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
69		inss1 3643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
70		elssuni 4219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
71	70	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
72	69, 71	syl5ss 3429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
73		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
74	73	inex1 4537	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
75	74	elpw 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
76	72, 75	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
77	76	rgen2a 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
78	60	fmpt2 6879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
79	77, 78	mpbi 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
80		frn 5747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	79, 80	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	68, 81	ssexi 4541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
84		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
85		nfcv 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
86		dffi3.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
87		mpt2eq12 6370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
88	87	anidms 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
89		ineq1 3618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
90		ineq2 3619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
91	89, 90	cbvmpt2v 6390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
92	88, 91	syl6eq 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
93	92	rneqd 5068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
94	93	cbvmptv 4488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
95	86, 94	eqtri 2493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
96		rdgeq1 7147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
97	95, 96	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
98	97	reseq1i 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
99		mpt2eq12 6370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
100	99	anidms 657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
101	100	rneqd 5068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
102	83, 84, 85, 98, 101	frsucmpt 7173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
103	65, 82, 102	sylancl 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
104	64, 103	syl5sseqr 3467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
105		sstr2 3425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106	104, 105	syl5com 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
107	106	ralimdv 2806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
108		vex 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
109		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
110	109	sseq1d 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
111	108, 110	ralsn 4001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
112	104, 111	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
113	107, 112	jctird 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
114		df-suc 5436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
115	114	raleqi 2977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
116		ralunb 3606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
117	115, 116	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
118	113, 117	syl6ibr 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
119		fiin 7954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
120	119	rgen2a 2820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
121		ssralv 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
122	121	ralimdv 2806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
123		ssralv 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
124	122, 123	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
125	120, 124	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	60	fmpt2 6879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
127	125, 126	sylib 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128		frn 5747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
130	129	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
131	103, 130	eqsstrd 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
132	118, 131	jctild 552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
133	132	expimpd 614	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
134	133	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
135	37, 42, 47, 49, 134	finds2 6740	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
136	135	impcom 437	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
137	136	simprd 470	. . . . . . . . . . . . . . . . . . . . 21 $/\$
138	137	r19.21bi 2776	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
139	138	ex 441	. . . . . . . . . . . . . . . . . . 19 $/\$
140	139	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
141		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20
142		eqimss 3470	. . . . . . . . . . . . . . . . . . . 20
143	141, 142	syl 17	. . . . . . . . . . . . . . . . . . 19
144	143	a1i 11	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
145	140, 144	jaod 387	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\/$
146	32, 145	sylbid 223	. . . . . . . . . . . . . . . 16 $/\$ $/\$
147	146	ralrimiva 2809	. . . . . . . . . . . . . . 15 $/\$
148	147	ralrimiva 2809	. . . . . . . . . . . . . 14
149	148	adantr 472	. . . . . . . . . . . . 13 $/\$ $/\$
150		ssun1 3588	. . . . . . . . . . . . . 14
151	150	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
152		sseq2 3440	. . . . . . . . . . . . . . 15
153		fveq2 5879	. . . . . . . . . . . . . . . 16
154	153	sseq2d 3446	. . . . . . . . . . . . . . 15
155	152, 154	imbi12d 327	. . . . . . . . . . . . . 14
156		sseq1 3439	. . . . . . . . . . . . . . 15
157		fveq2 5879	. . . . . . . . . . . . . . . 16
158	157	sseq1d 3445	. . . . . . . . . . . . . . 15
159	156, 158	imbi12d 327	. . . . . . . . . . . . . 14
160	155, 159	rspc2v 3147	. . . . . . . . . . . . 13 $/\$
161	26, 149, 151, 160	syl3c 62	. . . . . . . . . . . 12 $/\$ $/\$
162	161	sseld 3417	. . . . . . . . . . 11 $/\$ $/\$
163		simprr 774	. . . . . . . . . . . . . 14 $/\$ $/\$
164	24, 163	jca 541	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
165		ssun2 3589	. . . . . . . . . . . . . 14
166	165	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$
167		sseq1 3439	. . . . . . . . . . . . . . 15
168	109	sseq1d 3445	. . . . . . . . . . . . . . 15
169	167, 168	imbi12d 327	. . . . . . . . . . . . . 14
170	155, 169	rspc2v 3147	. . . . . . . . . . . . 13 $/\$
171	164, 149, 166, 170	syl3c 62	. . . . . . . . . . . 12 $/\$ $/\$
172	171	sseld 3417	. . . . . . . . . . 11 $/\$ $/\$
173	23	ad2antlr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
174		peano2 6732	. . . . . . . . . . . . . . 15
175		fveq2 5879	. . . . . . . . . . . . . . . 16
176	175	ssiun2s 4313	. . . . . . . . . . . . . . 15
177	173, 174, 176	3syl 18	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
178		simprl 772	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
179		simprr 774	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
180		eqidd 2472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
181		ineq1 3618	. . . . . . . . . . . . . . . . . . . 20
182	181	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19
183		ineq2 3619	. . . . . . . . . . . . . . . . . . . 20
184	183	eqeq2d 2481	. . . . . . . . . . . . . . . . . . 19
185	182, 184	rspc2ev 3149	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
186	178, 179, 180, 185	syl3anc 1292	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
187		vex 3034	. . . . . . . . . . . . . . . . . . 19
188	187	inex1 4537	. . . . . . . . . . . . . . . . . 18
189		eqeq1 2475	. . . . . . . . . . . . . . . . . . 19
190	189	2rexbidv 2897	. . . . . . . . . . . . . . . . . 18
191	188, 190	elab 3173	. . . . . . . . . . . . . . . . 17
192	186, 191	sylibr 217	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
193		eqid 2471	. . . . . . . . . . . . . . . . 17
194	193	rnmpt2 6425	. . . . . . . . . . . . . . . 16
195	192, 194	syl6eleqr 2560	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
196		fvex 5889	. . . . . . . . . . . . . . . . . . 19
197	196	uniex 6606	. . . . . . . . . . . . . . . . . 18
198	197	pwex 4584	. . . . . . . . . . . . . . . . 17
199		elssuni 4219	. . . . . . . . . . . . . . . . . . . . . . 23
200	69, 199	syl5ss 3429	. . . . . . . . . . . . . . . . . . . . . 22
201	74	elpw 3948	. . . . . . . . . . . . . . . . . . . . . 22
202	200, 201	sylibr 217	. . . . . . . . . . . . . . . . . . . . 21
203	202	adantr 472	. . . . . . . . . . . . . . . . . . . 20 $/\$
204	203	rgen2a 2820	. . . . . . . . . . . . . . . . . . 19
205	193	fmpt2 6879	. . . . . . . . . . . . . . . . . . 19
206	204, 205	mpbi 213	. . . . . . . . . . . . . . . . . 18
207		frn 5747	. . . . . . . . . . . . . . . . . 18
208	206, 207	ax-mp 5	. . . . . . . . . . . . . . . . 17
209	198, 208	ssexi 4541	. . . . . . . . . . . . . . . 16
210		nfcv 2612	. . . . . . . . . . . . . . . . 17
211		nfcv 2612	. . . . . . . . . . . . . . . . 17
212		mpt2eq12 6370	. . . . . . . . . . . . . . . . . . 19 $/\$
213	212	anidms 657	. . . . . . . . . . . . . . . . . 18
214	213	rneqd 5068	. . . . . . . . . . . . . . . . 17
215	83, 210, 211, 98, 214	frsucmpt 7173	. . . . . . . . . . . . . . . 16 $/\$
216	173, 209, 215	sylancl 675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
217	195, 216	eleqtrrd 2552	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
218	177, 217	sseldd 3419	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
219		fniunfv 6170	. . . . . . . . . . . . . 14
220	3, 219	ax-mp 5	. . . . . . . . . . . . 13
221	218, 220	syl6eleq 2559	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
222	221	ex 441	. . . . . . . . . . 11 $/\$ $/\$ $/\$
223	162, 172, 222	syl2and 491	. . . . . . . . . 10 $/\$ $/\$ $/\$
224	223	rexlimdvva 2878	. . . . . . . . 9 $/\$
225	224	imp 436	. . . . . . . 8 $/\$ $/\$
226	20, 225	sylan2br 484	. . . . . . 7 $/\$ $/\$
227	226	ralrimivva 2814	. . . . . 6
228	136	simpld 466	. . . . . . . . . . . 12 $/\$
229		fvex 5889	. . . . . . . . . . . . 13
230	229	elpw2 4565	. . . . . . . . . . . 12
231	228, 230	sylibr 217	. . . . . . . . . . 11 $/\$
232	231	ralrimiva 2809	. . . . . . . . . 10
233		fnfvrnss 6066	. . . . . . . . . 10 $/\$
234	3, 232, 233	sylancr 676	. . . . . . . . 9
235		sspwuni 4360	. . . . . . . . 9
236	234, 235	sylib 201	. . . . . . . 8
237		ssexg 4542	. . . . . . . 8 $/\$
238	236, 229, 237	sylancl 675	. . . . . . 7
239		sseq2 3440	. . . . . . . . 9
240		eleq2 2538	. . . . . . . . . . 11
241	240	raleqbi1dv 2981	. . . . . . . . . 10
242	241	raleqbi1dv 2981	. . . . . . . . 9
243	239, 242	anbi12d 725	. . . . . . . 8 $/\$ $/\$
244	243	elabg 3174	. . . . . . 7 $/\$ $/\$
245	238, 244	syl 17	. . . . . 6 $/\$ $/\$
246	9, 227, 245	mpbir2and 936	. . . . 5 $/\$
247		intss1 4241	. . . . 5 $/\$ $/\$
248	246, 247	syl 17	. . . 4 $/\$
249	1, 248	eqsstrd 3452	. . 3
250	249, 236	eqssd 3435	. 2
251		df-ima 4852	. . 3
252	251	unieqi 4199	. 2
253	250, 252	syl6eqr 2523	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376

wceq 1452

wcel 1904

cab 2457

wral 2756

wrex 2757

cvv 3031

cun 3388

cin 3389

wss 3390

c0 3722

cpw 3942

csn 3959

cuni 4190

cint 4226

ciun 4269

cmpt 4454

cxp 4837

crn 4840

cres 4841

cima 4842

word 5429

con0 5430

csuc 5432

wfn 5584

wf 5585

cfv 5589

cmpt2 6310

com 6711

crdg 7145

cfi 7942

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-en 7588 df-fin 7591 df-fi 7943

This theorem is referenced by: (None)

W3C validator