filufint - Metamath Proof Explorer

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

Theorem filufint 20984

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 3060	. . . . 5
2	1	elintrab 4260	. . . 4
3		filsspw 20915	. . . . . . . . . . . . . 14
4	3	3ad2ant1 1035	. . . . . . . . . . . . 13 $/\$ $/\$
5		difss 3572	. . . . . . . . . . . . . . 15 $\$
6		filtop 20919	. . . . . . . . . . . . . . . . . 18
7		difexg 4565	. . . . . . . . . . . . . . . . . 18 $\$
8	6, 7	syl 17	. . . . . . . . . . . . . . . . 17 $\$
9	8	3ad2ant1 1035	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
10		elpwg 3971	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
11	9, 10	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
12	5, 11	mpbiri 241	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
13	12	snssd 4130	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
14	4, 13	unssd 3622	. . . . . . . . . . . 12 $/\$ $/\$ $\$
15		ssun1 3609	. . . . . . . . . . . . . 14 $\$
16		filn0 20926	. . . . . . . . . . . . . 14
17		ssn0 3779	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
18	15, 16, 17	sylancr 674	. . . . . . . . . . . . 13 $\$
19	18	3ad2ant1 1035	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20		elsni 4005	. . . . . . . . . . . . . . 15 $\$ $\$
21		filelss 20916	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	21	3adant3 1034	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23		reldisj 3820	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
24	22, 23	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $\$
25		dfss4 3689	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
26	25	biimpi 199	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
27	26	sseq2d 3472	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
28	27	3ad2ant3 1037	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
29	24, 28	bitrd 261	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
30		filss 20917	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
31	30	3exp2 1235	. . . . . . . . . . . . . . . . . . . . . . 23
32	31	3imp 1208	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
33	29, 32	sylbid 223	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
34	33	necon3bd 2650	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
35	34	3exp 1214	. . . . . . . . . . . . . . . . . . 19 $\$
36	35	com24 90	. . . . . . . . . . . . . . . . . 18 $\$
37	36	3imp1 1230	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
38		ineq2 3640	. . . . . . . . . . . . . . . . . 18 $\$ $\$
39	38	neeq1d 2695	. . . . . . . . . . . . . . . . 17 $\$ $\$
40	37, 39	syl5ibrcom 230	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
41	40	expimpd 612	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
42	20, 41	sylan2i 665	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
43	42	ralrimivv 2820	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
44		filfbas 20912	. . . . . . . . . . . . . . 15
45	44	3ad2ant1 1035	. . . . . . . . . . . . . 14 $/\$ $/\$
46	5	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
47	26	3ad2ant2 1036	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
48		difeq2 3557	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
49		dif0 3849	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
50	48, 49	syl6eq 2512	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
51	50	3ad2ant3 1037	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
52	47, 51	eqtr3d 2498	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
53	6	3ad2ant1 1035	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
54	52, 53	eqeltrd 2540	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
55	54	3expia 1217	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
56	55	necon3bd 2650	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
57	56	ex 440	. . . . . . . . . . . . . . . . 17 $\$
58	57	com23 81	. . . . . . . . . . . . . . . 16 $\$
59	58	3imp 1208	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
60	6	3ad2ant1 1035	. . . . . . . . . . . . . . 15 $/\$ $/\$
61		snfbas 20930	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
62	46, 59, 60, 61	syl3anc 1276	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
63		fbunfip 20933	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
64	45, 62, 63	syl2anc 671	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
65	43, 64	mpbird 240	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66		fsubbas 20931	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $/\$ $\$
67	6, 66	syl 17	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $/\$ $\$
68	67	3ad2ant1 1035	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
69	14, 19, 65, 68	mpbir3and 1197	. . . . . . . . . . 11 $/\$ $/\$ $\$
70		fgcl 20942	. . . . . . . . . . 11 $\$ $\$
71	69, 70	syl 17	. . . . . . . . . 10 $/\$ $/\$ $\$
72		filssufil 20976	. . . . . . . . . . 11 $\$ $\$
73		snex 4655	. . . . . . . . . . . . . . . . . . . . 21 $\$
74		unexg 6619	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
75	73, 74	mpan2 682	. . . . . . . . . . . . . . . . . . . 20 $\$
76		ssfii 7959	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
77	75, 76	syl 17	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
78	77	3ad2ant1 1035	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
79	78	unssad 3623	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
80		ssfg 20936	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
81	69, 80	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
82	79, 81	sstrd 3454	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
83	82	ad2antrr 737	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
84		simpr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
85	83, 84	sstrd 3454	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
86		ufilfil 20968	. . . . . . . . . . . . . . . . 17
87		0nelfil 20913	. . . . . . . . . . . . . . . . 17
88	86, 87	syl 17	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 738	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
90		disjdif 3851	. . . . . . . . . . . . . . . . 17 $\$
91	86	ad2antlr 738	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
92		simprr 771	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
93	77	unssbd 3624	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
94	93	3ad2ant1 1035	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
95	94	adantr 471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
96	69	adantr 471	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
97	96, 80	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
98	95, 97	sstrd 3454	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$
99	98	adantr 471	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
100		simprl 769	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
101	99, 100	sstrd 3454	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
102		snidg 4006	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
103	8, 102	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
104	103	3ad2ant1 1035	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$
105	104	ad2antrr 737	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
106	101, 105	sseldd 3445	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		filin 20918	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
108	91, 92, 106, 107	syl3anc 1276	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	90, 108	syl5eqelr 2545	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
110	109	expr 624	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
111	89, 110	mtod 182	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
112	85, 111	jca 539	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
113	112	exp31 613	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$
114	113	reximdvai 2871	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$
115	72, 114	syl5 33	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
116	71, 115	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
117	116	3expia 1217	. . . . . . . 8 $/\$ $/\$
118		filssufil 20976	. . . . . . . . . 10
119		filelss 20916	. . . . . . . . . . . . . . . . 17 $/\$
120	119	ex 440	. . . . . . . . . . . . . . . 16
121	86, 120	syl 17	. . . . . . . . . . . . . . 15
122	121	con3d 140	. . . . . . . . . . . . . 14
123	122	impcom 436	. . . . . . . . . . . . 13 $/\$
124	123	a1d 26	. . . . . . . . . . . 12 $/\$
125	124	ancld 560	. . . . . . . . . . 11 $/\$ $/\$
126	125	reximdva 2874	. . . . . . . . . 10 $/\$
127	118, 126	syl5com 31	. . . . . . . . 9 $/\$
128	127	adantr 471	. . . . . . . 8 $/\$ $/\$
129	117, 128	pm2.61d 163	. . . . . . 7 $/\$ $/\$
130	129	ex 440	. . . . . 6 $/\$
131		rexanali 2852	. . . . . 6 $/\$
132	130, 131	syl6ib 234	. . . . 5
133	132	con4d 109	. . . 4
134	2, 133	syl5bi 225	. . 3
135	134	ssrdv 3450	. 2
136		ssintub 4266	. . 3
137	136	a1i 11	. 2
138	135, 137	eqssd 3461	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

wne 2633

wral 2749

wrex 2750

crab 2753

cvv 3057 $\$ cdif 3413

cun 3414

cin 3415

wss 3416

c0 3743

cpw 3963

csn 3980

cint 4248

cfv 5601 (class class class)co 6315

cfi 7950

cfbas 19007

cfg 19008

cfil 20909

cufil 20963

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4529 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-ac2 8919

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-se 4813 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-isom 5610 df-riota 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-rpss 6598 df-om 6720 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-1o 7208 df-oadd 7212 df-er 7389 df-en 7596 df-dom 7597 df-fin 7599 df-fi 7951 df-card 8399 df-ac 8573 df-cda 8624 df-fbas 19016 df-fg 19017 df-fil 20910 df-ufil 20965

This theorem is referenced by: (None)

W3C validator