elfiun - Metamath Proof Explorer

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

Theorem elfiun 8336

Description: A finite intersection of elements taken from a union of collections. (Contributed by Jeff Hankins, 15-Nov-2009.) (Proof shortened by Mario Carneiro, 26-Nov-2013.)

**Assertion**
Ref	Expression
elfiun	$/\$ $\/$ $\/$

Distinct variable groups:

Proof of Theorem elfiun Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3212	. . . 4
2	1	adantl 482	. . 3 $/\$ $/\$
3		simpll 790	. . 3 $/\$ $/\$
4		simplr 792	. . 3 $/\$ $/\$
5	2, 3, 4	3jca 1242	. 2 $/\$ $/\$ $/\$ $/\$
6		elex 3212	. . . . . 6
7	6	3anim1i 1248	. . . . 5 $/\$ $/\$ $/\$ $/\$
8	7	3expib 1268	. . . 4 $/\$ $/\$ $/\$
9		elex 3212	. . . . . 6
10	9	3anim1i 1248	. . . . 5 $/\$ $/\$ $/\$ $/\$
11	10	3expib 1268	. . . 4 $/\$ $/\$ $/\$
12		vex 3203	. . . . . . . . . 10
13	12	inex1 4799	. . . . . . . . 9
14		eleq1 2689	. . . . . . . . 9
15	13, 14	mpbiri 248	. . . . . . . 8
16	15	a1i 11	. . . . . . 7 $/\$
17	16	rexlimivv 3036	. . . . . 6
18	17	3anim1i 1248	. . . . 5 $/\$ $/\$ $/\$ $/\$
19	18	3expib 1268	. . . 4 $/\$ $/\$ $/\$
20	8, 11, 19	3jaoi 1391	. . 3 $\/$ $\/$ $/\$ $/\$ $/\$
21	20	impcom 446	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $/\$
22		simp1 1061	. . . . 5 $/\$ $/\$
23		unexg 6959	. . . . . 6 $/\$
24	23	3adant1 1079	. . . . 5 $/\$ $/\$
25		elfi 8319	. . . . 5 $/\$
26	22, 24, 25	syl2anc 693	. . . 4 $/\$ $/\$
27		simpl1 1064	. . . . . . 7 $/\$ $/\$ $/\$
28		eleq1 2689	. . . . . . . 8
29		intex 4820	. . . . . . . 8
30	28, 29	syl6bbr 278	. . . . . . 7
31	27, 30	syl5ibcom 235	. . . . . 6 $/\$ $/\$ $/\$
32		simp22 1095	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
33		inss2 3834	. . . . . . . . . . . . . . 15
34	33	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		simp1l 1085	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
36		simp3l 1089	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37		inss2 3834	. . . . . . . . . . . . . . . . 17
38	37	sseli 3599	. . . . . . . . . . . . . . . 16
39	36, 38	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		inss1 3833	. . . . . . . . . . . . . . 15
41		ssfi 8180	. . . . . . . . . . . . . . 15 $/\$
42	39, 40, 41	sylancl 694	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43		elfir 8321	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
44	32, 34, 35, 42, 43	syl13anc 1328	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp23 1096	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46		inss2 3834	. . . . . . . . . . . . . . 15
47	46	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48		simp1r 1086	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		inss1 3833	. . . . . . . . . . . . . . 15
50		ssfi 8180	. . . . . . . . . . . . . . 15 $/\$
51	39, 49, 50	sylancl 694	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52		elfir 8321	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
53	45, 47, 48, 51, 52	syl13anc 1328	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54		inss1 3833	. . . . . . . . . . . . . . . 16
55	54	sseli 3599	. . . . . . . . . . . . . . 15
56	55	elpwid 4170	. . . . . . . . . . . . . 14
57		indi 3873	. . . . . . . . . . . . . . . . 17
58		df-ss 3588	. . . . . . . . . . . . . . . . . 18
59	58	biimpi 206	. . . . . . . . . . . . . . . . 17
60	57, 59	syl5reqr 2671	. . . . . . . . . . . . . . . 16
61	60	inteqd 4480	. . . . . . . . . . . . . . 15
62		intun 4509	. . . . . . . . . . . . . . 15
63	61, 62	syl6eq 2672	. . . . . . . . . . . . . 14
64	36, 56, 63	3syl 18	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
65		ineq1 3807	. . . . . . . . . . . . . . 15
66	65	eqeq2d 2632	. . . . . . . . . . . . . 14
67		ineq2 3808	. . . . . . . . . . . . . . 15
68	67	eqeq2d 2632	. . . . . . . . . . . . . 14
69	66, 68	rspc2ev 3324	. . . . . . . . . . . . 13 $/\$ $/\$
70	44, 53, 64, 69	syl3anc 1326	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70	3mix3d 1238	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
72	71	3expib 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
73		simp23 1096	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
74		simp1 1061	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
75		simp3l 1089	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
76		reldisj 4020	. . . . . . . . . . . . . . . 16 $\$
77	75, 56, 76	3syl 18	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
78	74, 77	mpbid 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
79		uncom 3757	. . . . . . . . . . . . . . . . 17
80	79	difeq1i 3724	. . . . . . . . . . . . . . . 16 $\$ $\$
81		difun2 4048	. . . . . . . . . . . . . . . 16 $\$ $\$
82	80, 81	eqtri 2644	. . . . . . . . . . . . . . 15 $\$ $\$
83		difss 3737	. . . . . . . . . . . . . . 15 $\$
84	82, 83	eqsstri 3635	. . . . . . . . . . . . . 14 $\$
85	78, 84	syl6ss 3615	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
86		simp3r 1090	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
87	75, 38	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
88		elfir 8321	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
89	73, 85, 86, 87, 88	syl13anc 1328	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
90	89	3mix2d 1237	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
91	90	3expib 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
92		simp22 1095	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
93		simp1 1061	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
94		simp3l 1089	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
95		reldisj 4020	. . . . . . . . . . . . . . . 16 $\$
96	94, 56, 95	3syl 18	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
97	93, 96	mpbid 222	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
98		difun2 4048	. . . . . . . . . . . . . . 15 $\$ $\$
99		difss 3737	. . . . . . . . . . . . . . 15 $\$
100	98, 99	eqsstri 3635	. . . . . . . . . . . . . 14 $\$
101	97, 100	syl6ss 3615	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
102		simp3r 1090	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
103	94, 38	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
104		elfir 8321	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
105	92, 101, 102, 103, 104	syl13anc 1328	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
106	105	3mix1d 1236	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
107	106	3expib 1268	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
108	72, 91, 107	pm2.61iine 2884	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
109		eleq1 2689	. . . . . . . . . 10
110		eleq1 2689	. . . . . . . . . 10
111		eqeq1 2626	. . . . . . . . . . 11
112	111	2rexbidv 3057	. . . . . . . . . 10
113	109, 110, 112	3orbi123d 1398	. . . . . . . . 9 $\/$ $\/$ $\/$ $\/$
114	108, 113	syl5ibrcom 237	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
115	114	expr 643	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $\/$
116	115	com23 86	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $\/$
117	31, 116	mpdd 43	. . . . 5 $/\$ $/\$ $/\$ $\/$ $\/$
118	117	rexlimdva 3031	. . . 4 $/\$ $/\$ $\/$ $\/$
119	26, 118	sylbid 230	. . 3 $/\$ $/\$ $\/$ $\/$
120		ssun1 3776	. . . . . . 7
121		fiss 8330	. . . . . . 7 $/\$
122	23, 120, 121	sylancl 694	. . . . . 6 $/\$
123	122	3adant1 1079	. . . . 5 $/\$ $/\$
124	123	sseld 3602	. . . 4 $/\$ $/\$
125		ssun2 3777	. . . . . . 7
126		fiss 8330	. . . . . . 7 $/\$
127	23, 125, 126	sylancl 694	. . . . . 6 $/\$
128	127	3adant1 1079	. . . . 5 $/\$ $/\$
129	128	sseld 3602	. . . 4 $/\$ $/\$
130	123	sseld 3602	. . . . . . 7 $/\$ $/\$
131	128	sseld 3602	. . . . . . 7 $/\$ $/\$
132	130, 131	anim12d 586	. . . . . 6 $/\$ $/\$ $/\$ $/\$
133		fiin 8328	. . . . . . 7 $/\$
134		eleq1a 2696	. . . . . . 7
135	133, 134	syl 17	. . . . . 6 $/\$
136	132, 135	syl6 35	. . . . 5 $/\$ $/\$ $/\$
137	136	rexlimdvv 3037	. . . 4 $/\$ $/\$
138	124, 129, 137	3jaod 1392	. . 3 $/\$ $/\$ $\/$ $\/$
139	119, 138	impbid 202	. 2 $/\$ $/\$ $\/$ $\/$
140	5, 21, 139	pm5.21nd 941	1 $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384 $\/$ w3o 1036 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wrex 2913

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cpw 4158

cint 4475

cfv 5888

cfn 7955

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-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: ordtbas2 20995 ordtbas 20996 fbunfip 21673 fmfnfmlem4 21761

W3C validator