filufint - Metamath Proof Explorer

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

Theorem filufint 20149

Description: A filter is equal to the intersection of the ultrafilters containing it. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Stefan O'Rear, 2-Aug-2015.)

**Assertion**
Ref	Expression
filufint

Distinct variable groups:

Proof of Theorem filufint Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3109	. . . . 5
2	1	elintrab 4287	. . . 4
3		filsspw 20080	. . . . . . . . . . . . . 14
4	3	3ad2ant1 1012	. . . . . . . . . . . . 13 $/\$ $/\$
5		difss 3624	. . . . . . . . . . . . . . 15 $\$
6		filtop 20084	. . . . . . . . . . . . . . . . . 18
7		difexg 4588	. . . . . . . . . . . . . . . . . 18 $\$
8	6, 7	syl 16	. . . . . . . . . . . . . . . . 17 $\$
9	8	3ad2ant1 1012	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
10		elpwg 4011	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
11	9, 10	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
12	5, 11	mpbiri 233	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
13	12	snssd 4165	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
14	4, 13	unssd 3673	. . . . . . . . . . . 12 $/\$ $/\$ $\$
15		ssun1 3660	. . . . . . . . . . . . . 14 $\$
16		filn0 20091	. . . . . . . . . . . . . 14
17		ssn0 3811	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
18	15, 16, 17	sylancr 663	. . . . . . . . . . . . 13 $\$
19	18	3ad2ant1 1012	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20		elsni 4045	. . . . . . . . . . . . . . 15 $\$ $\$
21		filelss 20081	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	21	3adant3 1011	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23		reldisj 3863	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
24	22, 23	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $\$
25		dfss4 3725	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
26	25	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
27	26	sseq2d 3525	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
28	27	3ad2ant3 1014	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
29	24, 28	bitrd 253	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
30		filss 20082	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
31	30	3exp2 1209	. . . . . . . . . . . . . . . . . . . . . . 23
32	31	3imp 1185	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
33	29, 32	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
34	33	necon3bd 2672	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
35	34	3exp 1190	. . . . . . . . . . . . . . . . . . 19 $\$
36	35	com24 87	. . . . . . . . . . . . . . . . . 18 $\$
37	36	3imp1 1204	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
38		ineq2 3687	. . . . . . . . . . . . . . . . . 18 $\$ $\$
39	38	neeq1d 2737	. . . . . . . . . . . . . . . . 17 $\$ $\$
40	37, 39	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
41	40	expimpd 603	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
42	20, 41	sylan2i 655	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
43	42	ralrimivv 2877	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
44		filfbas 20077	. . . . . . . . . . . . . . 15
45	44	3ad2ant1 1012	. . . . . . . . . . . . . 14 $/\$ $/\$
46	5	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
47	26	3ad2ant2 1013	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
48		difeq2 3609	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
49		dif0 3890	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
50	48, 49	syl6eq 2517	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
51	50	3ad2ant3 1014	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
52	47, 51	eqtr3d 2503	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
53	6	3ad2ant1 1012	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
54	52, 53	eqeltrd 2548	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
55	54	3expia 1193	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
56	55	necon3bd 2672	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
57	56	ex 434	. . . . . . . . . . . . . . . . 17 $\$
58	57	com23 78	. . . . . . . . . . . . . . . 16 $\$
59	58	3imp 1185	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
60	6	3ad2ant1 1012	. . . . . . . . . . . . . . 15 $/\$ $/\$
61		snfbas 20095	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
62	46, 59, 60, 61	syl3anc 1223	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
63		fbunfip 20098	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
64	45, 62, 63	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
65	43, 64	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66		fsubbas 20096	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $/\$ $\$
67	6, 66	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $/\$ $\$
68	67	3ad2ant1 1012	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
69	14, 19, 65, 68	mpbir3and 1174	. . . . . . . . . . 11 $/\$ $/\$ $\$
70		fgcl 20107	. . . . . . . . . . 11 $\$ $\$
71	69, 70	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\$
72		filssufil 20141	. . . . . . . . . . 11 $\$ $\$
73		snex 4681	. . . . . . . . . . . . . . . . . . . . 21 $\$
74		unexg 6576	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
75	73, 74	mpan2 671	. . . . . . . . . . . . . . . . . . . 20 $\$
76		ssfii 7868	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
78	77	3ad2ant1 1012	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
79	78	unssad 3674	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
80		ssfg 20101	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
81	69, 80	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
82	79, 81	sstrd 3507	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
83	82	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
84		simpr 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
85	83, 84	sstrd 3507	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
86		ufilfil 20133	. . . . . . . . . . . . . . . . 17
87		0nelfil 20078	. . . . . . . . . . . . . . . . 17
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
90		disjdif 3892	. . . . . . . . . . . . . . . . 17 $\$
91	86	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
92		simprr 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
93	77	unssbd 3675	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
94	93	3ad2ant1 1012	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
95	94	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
96	69	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
97	96, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
98	95, 97	sstrd 3507	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$
99	98	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
100		simprl 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
101	99, 100	sstrd 3507	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
102		snidg 4046	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
103	8, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
104	103	3ad2ant1 1012	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$
105	104	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
106	101, 105	sseldd 3498	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		filin 20083	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
108	91, 92, 106, 107	syl3anc 1223	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	90, 108	syl5eqelr 2553	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
110	109	expr 615	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
111	89, 110	mtod 177	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
112	85, 111	jca 532	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
113	112	exp31 604	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$
114	113	reximdvai 2928	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$
115	72, 114	syl5 32	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
116	71, 115	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
117	116	3expia 1193	. . . . . . . 8 $/\$ $/\$
118		filssufil 20141	. . . . . . . . . 10
119		filelss 20081	. . . . . . . . . . . . . . . . 17 $/\$
120	119	ex 434	. . . . . . . . . . . . . . . 16
121	86, 120	syl 16	. . . . . . . . . . . . . . 15
122	121	con3d 133	. . . . . . . . . . . . . 14
123	122	impcom 430	. . . . . . . . . . . . 13 $/\$
124	123	a1d 25	. . . . . . . . . . . 12 $/\$
125	124	ancld 553	. . . . . . . . . . 11 $/\$ $/\$
126	125	reximdva 2931	. . . . . . . . . 10 $/\$
127	118, 126	syl5com 30	. . . . . . . . 9 $/\$
128	127	adantr 465	. . . . . . . 8 $/\$ $/\$
129	117, 128	pm2.61d 158	. . . . . . 7 $/\$ $/\$
130	129	ex 434	. . . . . 6 $/\$
131		rexanali 2910	. . . . . 6 $/\$
132	130, 131	syl6ib 226	. . . . 5
133	132	con4d 105	. . . 4
134	2, 133	syl5bi 217	. . 3
135	134	ssrdv 3503	. 2
136		ssintub 4293	. . 3
137	136	a1i 11	. 2
138	135, 137	eqssd 3514	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 968

wceq 1374

wcel 1762

wne 2655

wral 2807

wrex 2808

crab 2811

cvv 3106 $\$ cdif 3466

cun 3467

cin 3468

wss 3469

c0 3778

cpw 4003

csn 4020

cint 4275

cfv 5579 (class class class)co 6275

cfi 7859

cfbas 18170

cfg 18171

cfil 20074

cufil 20128

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-rep 4551 ax-sep 4561 ax-nul 4569 ax-pow 4618 ax-pr 4679 ax-un 6567 ax-ac2 8832

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-nel 2658 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3108 df-sbc 3325 df-csb 3429 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-int 4276 df-iun 4320 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-se 4832 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-f 5583 df-f1 5584 df-fo 5585 df-f1o 5586 df-fv 5587 df-isom 5588 df-riota 6236 df-ov 6278 df-oprab 6279 df-mpt2 6280 df-rpss 6555 df-om 6672 df-recs 7032 df-rdg 7066 df-1o 7120 df-oadd 7124 df-er 7301 df-en 7507 df-dom 7508 df-fin 7510 df-fi 7860 df-card 8309 df-ac 8486 df-cda 8537 df-fbas 18180 df-fg 18181 df-fil 20075 df-ufil 20130

This theorem is referenced by: (None)

W3C validator