filufint - Metamath Proof Explorer

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

Theorem filufint 19496

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 2978	. . . . 5
2	1	elintrab 4143	. . . 4
3		filsspw 19427	. . . . . . . . . . . . . 14
4	3	3ad2ant1 1009	. . . . . . . . . . . . 13 $/\$ $/\$
5		difss 3486	. . . . . . . . . . . . . . 15 $\$
6		filtop 19431	. . . . . . . . . . . . . . . . . 18
7		difexg 4443	. . . . . . . . . . . . . . . . . 18 $\$
8	6, 7	syl 16	. . . . . . . . . . . . . . . . 17 $\$
9	8	3ad2ant1 1009	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
10		elpwg 3871	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
11	9, 10	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
12	5, 11	mpbiri 233	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
13	12	snssd 4021	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
14	4, 13	unssd 3535	. . . . . . . . . . . 12 $/\$ $/\$ $\$
15		ssun1 3522	. . . . . . . . . . . . . 14 $\$
16		filn0 19438	. . . . . . . . . . . . . 14
17		ssn0 3673	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
18	15, 16, 17	sylancr 663	. . . . . . . . . . . . 13 $\$
19	18	3ad2ant1 1009	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20		elsni 3905	. . . . . . . . . . . . . . 15 $\$ $\$
21		filelss 19428	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	21	3adant3 1008	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23		reldisj 3725	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
24	22, 23	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $\$
25		dfss4 3587	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
26	25	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
27	26	sseq2d 3387	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
28	27	3ad2ant3 1011	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
29	24, 28	bitrd 253	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
30		filss 19429	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
31	30	3exp2 1205	. . . . . . . . . . . . . . . . . . . . . . 23
32	31	3imp 1181	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
33	29, 32	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
34	33	necon3bd 2648	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
35	34	3exp 1186	. . . . . . . . . . . . . . . . . . 19 $\$
36	35	com24 87	. . . . . . . . . . . . . . . . . 18 $\$
37	36	3imp1 1200	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
38		ineq2 3549	. . . . . . . . . . . . . . . . . 18 $\$ $\$
39	38	neeq1d 2624	. . . . . . . . . . . . . . . . 17 $\$ $\$
40	37, 39	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
41	40	expimpd 603	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
42	20, 41	sylan2i 655	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
43	42	ralrimivv 2810	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
44		filfbas 19424	. . . . . . . . . . . . . . 15
45	44	3ad2ant1 1009	. . . . . . . . . . . . . 14 $/\$ $/\$
46	5	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
47	26	3ad2ant2 1010	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
48		difeq2 3471	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
49		dif0 3752	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
50	48, 49	syl6eq 2491	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
51	50	3ad2ant3 1011	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
52	47, 51	eqtr3d 2477	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
53	6	3ad2ant1 1009	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
54	52, 53	eqeltrd 2517	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
55	54	3expia 1189	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
56	55	necon3bd 2648	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
57	56	ex 434	. . . . . . . . . . . . . . . . 17 $\$
58	57	com23 78	. . . . . . . . . . . . . . . 16 $\$
59	58	3imp 1181	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
60	6	3ad2ant1 1009	. . . . . . . . . . . . . . 15 $/\$ $/\$
61		snfbas 19442	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
62	46, 59, 60, 61	syl3anc 1218	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
63		fbunfip 19445	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
64	45, 62, 63	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
65	43, 64	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66		fsubbas 19443	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $/\$ $\$
67	6, 66	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $/\$ $\$
68	67	3ad2ant1 1009	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
69	14, 19, 65, 68	mpbir3and 1171	. . . . . . . . . . 11 $/\$ $/\$ $\$
70		fgcl 19454	. . . . . . . . . . 11 $\$ $\$
71	69, 70	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\$
72		filssufil 19488	. . . . . . . . . . 11 $\$ $\$
73		snex 4536	. . . . . . . . . . . . . . . . . . . . 21 $\$
74		unexg 6384	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
75	73, 74	mpan2 671	. . . . . . . . . . . . . . . . . . . 20 $\$
76		ssfii 7672	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
78	77	3ad2ant1 1009	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
79	78	unssad 3536	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
80		ssfg 19448	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
81	69, 80	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
82	79, 81	sstrd 3369	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
83	82	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
84		simpr 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
85	83, 84	sstrd 3369	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
86		ufilfil 19480	. . . . . . . . . . . . . . . . 17
87		0nelfil 19425	. . . . . . . . . . . . . . . . 17
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
90		disjdif 3754	. . . . . . . . . . . . . . . . 17 $\$
91	86	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
92		simprr 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
93	77	unssbd 3537	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
94	93	3ad2ant1 1009	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
95	94	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
96	69	adantr 465	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
97	96, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
98	95, 97	sstrd 3369	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$
99	98	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
100		simprl 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
101	99, 100	sstrd 3369	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
102		snidg 3906	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
103	8, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
104	103	3ad2ant1 1009	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$
105	104	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
106	101, 105	sseldd 3360	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		filin 19430	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
108	91, 92, 106, 107	syl3anc 1218	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	90, 108	syl5eqelr 2528	. . . . . . . . . . . . . . . 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 2829	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$
115	72, 114	syl5 32	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
116	71, 115	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
117	116	3expia 1189	. . . . . . . 8 $/\$ $/\$
118		filssufil 19488	. . . . . . . . . 10
119		filelss 19428	. . . . . . . . . . . . . . . . 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 2831	. . . . . . . . . 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 2764	. . . . . 6 $/\$
132	130, 131	syl6ib 226	. . . . 5
133	132	con4d 105	. . . 4
134	2, 133	syl5bi 217	. . 3
135	134	ssrdv 3365	. 2
136		ssintub 4149	. . 3
137	136	a1i 11	. 2
138	135, 137	eqssd 3376	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2609

wral 2718

wrex 2719

crab 2722

cvv 2975 $\$ cdif 3328

cun 3329

cin 3330

wss 3331

c0 3640

cpw 3863

csn 3880

cint 4131

cfv 5421 (class class class)co 6094

cfi 7663

cfbas 17807

cfg 17808

cfil 19421

cufil 19475

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4406 ax-sep 4416 ax-nul 4424 ax-pow 4473 ax-pr 4534 ax-un 6375 ax-ac2 8635

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2571 df-ne 2611 df-nel 2612 df-ral 2723 df-rex 2724 df-reu 2725 df-rmo 2726 df-rab 2727 df-v 2977 df-sbc 3190 df-csb 3292 df-dif 3334 df-un 3336 df-in 3338 df-ss 3345 df-pss 3347 df-nul 3641 df-if 3795 df-pw 3865 df-sn 3881 df-pr 3883 df-tp 3885 df-op 3887 df-uni 4095 df-int 4132 df-iun 4176 df-br 4296 df-opab 4354 df-mpt 4355 df-tr 4389 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-se 4683 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4849 df-rel 4850 df-cnv 4851 df-co 4852 df-dm 4853 df-rn 4854 df-res 4855 df-ima 4856 df-iota 5384 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-isom 5430 df-riota 6055 df-ov 6097 df-oprab 6098 df-mpt2 6099 df-rpss 6363 df-om 6480 df-recs 6835 df-rdg 6869 df-1o 6923 df-oadd 6927 df-er 7104 df-en 7314 df-dom 7315 df-fin 7317 df-fi 7664 df-card 8112 df-ac 8289 df-cda 8340 df-fbas 17817 df-fg 17818 df-fil 19422 df-ufil 19477

This theorem is referenced by: (None)

W3C validator