filufint - Metamath Proof Explorer

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

Theorem filufint 20294

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 3098	. . . . 5
2	1	elintrab 4283	. . . 4
3		filsspw 20225	. . . . . . . . . . . . . 14
4	3	3ad2ant1 1018	. . . . . . . . . . . . 13 $/\$ $/\$
5		difss 3616	. . . . . . . . . . . . . . 15 $\$
6		filtop 20229	. . . . . . . . . . . . . . . . . 18
7		difexg 4585	. . . . . . . . . . . . . . . . . 18 $\$
8	6, 7	syl 16	. . . . . . . . . . . . . . . . 17 $\$
9	8	3ad2ant1 1018	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
10		elpwg 4005	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
11	9, 10	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
12	5, 11	mpbiri 233	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
13	12	snssd 4160	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
14	4, 13	unssd 3665	. . . . . . . . . . . 12 $/\$ $/\$ $\$
15		ssun1 3652	. . . . . . . . . . . . . 14 $\$
16		filn0 20236	. . . . . . . . . . . . . 14
17		ssn0 3804	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
18	15, 16, 17	sylancr 663	. . . . . . . . . . . . 13 $\$
19	18	3ad2ant1 1018	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20		elsni 4039	. . . . . . . . . . . . . . 15 $\$ $\$
21		filelss 20226	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	21	3adant3 1017	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23		reldisj 3856	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
24	22, 23	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $\$
25		dfss4 3717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
26	25	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
27	26	sseq2d 3517	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
28	27	3ad2ant3 1020	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
29	24, 28	bitrd 253	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
30		filss 20227	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
31	30	3exp2 1215	. . . . . . . . . . . . . . . . . . . . . . 23
32	31	3imp 1191	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
33	29, 32	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
34	33	necon3bd 2655	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
35	34	3exp 1196	. . . . . . . . . . . . . . . . . . 19 $\$
36	35	com24 87	. . . . . . . . . . . . . . . . . 18 $\$
37	36	3imp1 1210	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
38		ineq2 3679	. . . . . . . . . . . . . . . . . 18 $\$ $\$
39	38	neeq1d 2720	. . . . . . . . . . . . . . . . 17 $\$ $\$
40	37, 39	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
41	40	expimpd 603	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
42	20, 41	sylan2i 655	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
43	42	ralrimivv 2863	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
44		filfbas 20222	. . . . . . . . . . . . . . 15
45	44	3ad2ant1 1018	. . . . . . . . . . . . . 14 $/\$ $/\$
46	5	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
47	26	3ad2ant2 1019	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
48		difeq2 3601	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
49		dif0 3884	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
50	48, 49	syl6eq 2500	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
51	50	3ad2ant3 1020	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
52	47, 51	eqtr3d 2486	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
53	6	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
54	52, 53	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
55	54	3expia 1199	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
56	55	necon3bd 2655	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
57	56	ex 434	. . . . . . . . . . . . . . . . 17 $\$
58	57	com23 78	. . . . . . . . . . . . . . . 16 $\$
59	58	3imp 1191	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
60	6	3ad2ant1 1018	. . . . . . . . . . . . . . 15 $/\$ $/\$
61		snfbas 20240	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
62	46, 59, 60, 61	syl3anc 1229	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
63		fbunfip 20243	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
64	45, 62, 63	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
65	43, 64	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66		fsubbas 20241	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $/\$ $\$
67	6, 66	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $/\$ $\$
68	67	3ad2ant1 1018	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
69	14, 19, 65, 68	mpbir3and 1180	. . . . . . . . . . 11 $/\$ $/\$ $\$
70		fgcl 20252	. . . . . . . . . . 11 $\$ $\$
71	69, 70	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\$
72		filssufil 20286	. . . . . . . . . . 11 $\$ $\$
73		snex 4678	. . . . . . . . . . . . . . . . . . . . 21 $\$
74		unexg 6586	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
75	73, 74	mpan2 671	. . . . . . . . . . . . . . . . . . . 20 $\$
76		ssfii 7881	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
78	77	3ad2ant1 1018	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
79	78	unssad 3666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
80		ssfg 20246	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
81	69, 80	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
82	79, 81	sstrd 3499	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
83	82	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
84		simpr 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
85	83, 84	sstrd 3499	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
86		ufilfil 20278	. . . . . . . . . . . . . . . . 17
87		0nelfil 20223	. . . . . . . . . . . . . . . . 17
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
90		disjdif 3886	. . . . . . . . . . . . . . . . 17 $\$
91	86	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
92		simprr 757	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
93	77	unssbd 3667	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
94	93	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
95	94	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
96	69	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
97	96, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
98	95, 97	sstrd 3499	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$
99	98	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
100		simprl 756	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
101	99, 100	sstrd 3499	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
102		snidg 4040	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
103	8, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
104	103	3ad2ant1 1018	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$
105	104	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
106	101, 105	sseldd 3490	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		filin 20228	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
108	91, 92, 106, 107	syl3anc 1229	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	90, 108	syl5eqelr 2536	. . . . . . . . . . . . . . . 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 2915	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$
115	72, 114	syl5 32	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
116	71, 115	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
117	116	3expia 1199	. . . . . . . 8 $/\$ $/\$
118		filssufil 20286	. . . . . . . . . 10
119		filelss 20226	. . . . . . . . . . . . . . . . 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 2918	. . . . . . . . . 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 2896	. . . . . 6 $/\$
132	130, 131	syl6ib 226	. . . . 5
133	132	con4d 105	. . . 4
134	2, 133	syl5bi 217	. . 3
135	134	ssrdv 3495	. 2
136		ssintub 4289	. . 3
137	136	a1i 11	. 2
138	135, 137	eqssd 3506	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1383

wcel 1804

wne 2638

wral 2793

wrex 2794

crab 2797

cvv 3095 $\$ cdif 3458

cun 3459

cin 3460

wss 3461

c0 3770

cpw 3997

csn 4014

cint 4271

cfv 5578 (class class class)co 6281

cfi 7872

cfbas 18280

cfg 18281

cfil 20219

cufil 20273

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-ac2 8846

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-rpss 6565 df-om 6686 df-recs 7044 df-rdg 7078 df-1o 7132 df-oadd 7136 df-er 7313 df-en 7519 df-dom 7520 df-fin 7522 df-fi 7873 df-card 8323 df-ac 8500 df-cda 8551 df-fbas 18290 df-fg 18291 df-fil 20220 df-ufil 20275

This theorem is referenced by: (None)

W3C validator