filufint - Metamath Proof Explorer

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

Theorem filufint 19462

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 2969	. . . . 5
2	1	elintrab 4133	. . . 4
3		filsspw 19393	. . . . . . . . . . . . . 14
4	3	3ad2ant1 1009	. . . . . . . . . . . . 13 $/\$ $/\$
5		difss 3476	. . . . . . . . . . . . . . 15 $\$
6		filtop 19397	. . . . . . . . . . . . . . . . . 18
7		difexg 4433	. . . . . . . . . . . . . . . . . 18 $\$
8	6, 7	syl 16	. . . . . . . . . . . . . . . . 17 $\$
9	8	3ad2ant1 1009	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
10		elpwg 3861	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
11	9, 10	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
12	5, 11	mpbiri 233	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
13	12	snssd 4011	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
14	4, 13	unssd 3525	. . . . . . . . . . . 12 $/\$ $/\$ $\$
15		ssun1 3512	. . . . . . . . . . . . . 14 $\$
16		filn0 19404	. . . . . . . . . . . . . 14
17		ssn0 3663	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
18	15, 16, 17	sylancr 663	. . . . . . . . . . . . 13 $\$
19	18	3ad2ant1 1009	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20		elsni 3895	. . . . . . . . . . . . . . 15 $\$ $\$
21		filelss 19394	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	21	3adant3 1008	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23		reldisj 3715	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
24	22, 23	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $\$
25		dfss4 3577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
26	25	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
27	26	sseq2d 3377	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
28	27	3ad2ant3 1011	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
29	24, 28	bitrd 253	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
30		filss 19395	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
31	30	3exp2 1205	. . . . . . . . . . . . . . . . . . . . . . 23
32	31	3imp 1181	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
33	29, 32	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
34	33	necon3bd 2639	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
35	34	3exp 1186	. . . . . . . . . . . . . . . . . . 19 $\$
36	35	com24 87	. . . . . . . . . . . . . . . . . 18 $\$
37	36	3imp1 1200	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
38		ineq2 3539	. . . . . . . . . . . . . . . . . 18 $\$ $\$
39	38	neeq1d 2615	. . . . . . . . . . . . . . . . 17 $\$ $\$
40	37, 39	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
41	40	expimpd 603	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
42	20, 41	sylan2i 655	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
43	42	ralrimivv 2801	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
44		filfbas 19390	. . . . . . . . . . . . . . 15
45	44	3ad2ant1 1009	. . . . . . . . . . . . . 14 $/\$ $/\$
46	5	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
47	26	3ad2ant2 1010	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
48		difeq2 3461	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
49		dif0 3742	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
50	48, 49	syl6eq 2485	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
51	50	3ad2ant3 1011	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
52	47, 51	eqtr3d 2471	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
53	6	3ad2ant1 1009	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
54	52, 53	eqeltrd 2511	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
55	54	3expia 1189	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
56	55	necon3bd 2639	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
57	56	ex 434	. . . . . . . . . . . . . . . . 17 $\$
58	57	com23 78	. . . . . . . . . . . . . . . 16 $\$
59	58	3imp 1181	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
60	6	3ad2ant1 1009	. . . . . . . . . . . . . . 15 $/\$ $/\$
61		snfbas 19408	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
62	46, 59, 60, 61	syl3anc 1218	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
63		fbunfip 19411	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
64	45, 62, 63	syl2anc 661	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
65	43, 64	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66		fsubbas 19409	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $/\$ $\$
67	6, 66	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $/\$ $\$
68	67	3ad2ant1 1009	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
69	14, 19, 65, 68	mpbir3and 1171	. . . . . . . . . . 11 $/\$ $/\$ $\$
70		fgcl 19420	. . . . . . . . . . 11 $\$ $\$
71	69, 70	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\$
72		filssufil 19454	. . . . . . . . . . 11 $\$ $\$
73		snex 4526	. . . . . . . . . . . . . . . . . . . . 21 $\$
74		unexg 6376	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
75	73, 74	mpan2 671	. . . . . . . . . . . . . . . . . . . 20 $\$
76		ssfii 7661	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
78	77	3ad2ant1 1009	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
79	78	unssad 3526	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
80		ssfg 19414	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
81	69, 80	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
82	79, 81	sstrd 3359	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
83	82	ad2antrr 725	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
84		simpr 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
85	83, 84	sstrd 3359	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
86		ufilfil 19446	. . . . . . . . . . . . . . . . 17
87		0nelfil 19391	. . . . . . . . . . . . . . . . 17
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 726	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
90		disjdif 3744	. . . . . . . . . . . . . . . . 17 $\$
91	86	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
92		simprr 756	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
93	77	unssbd 3527	. . . . . . . . . . . . . . . . . . . . . . . 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 3359	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$
99	98	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
100		simprl 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
101	99, 100	sstrd 3359	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
102		snidg 3896	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
103	8, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
104	103	3ad2ant1 1009	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$
105	104	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
106	101, 105	sseldd 3350	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		filin 19396	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
108	91, 92, 106, 107	syl3anc 1218	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	90, 108	syl5eqelr 2522	. . . . . . . . . . . . . . . 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 2820	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$
115	72, 114	syl5 32	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
116	71, 115	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
117	116	3expia 1189	. . . . . . . 8 $/\$ $/\$
118		filssufil 19454	. . . . . . . . . 10
119		filelss 19394	. . . . . . . . . . . . . . . . 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 2822	. . . . . . . . . 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 2755	. . . . . 6 $/\$
132	130, 131	syl6ib 226	. . . . 5
133	132	con4d 105	. . . 4
134	2, 133	syl5bi 217	. . 3
135	134	ssrdv 3355	. 2
136		ssintub 4139	. . 3
137	136	a1i 11	. 2
138	135, 137	eqssd 3366	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2600

wral 2709

wrex 2710

crab 2713

cvv 2966 $\$ cdif 3318

cun 3319

cin 3320

wss 3321

c0 3630

cpw 3853

csn 3870

cint 4121

cfv 5411 (class class class)co 6086

cfi 7652

cfbas 17773

cfg 17774

cfil 19387

cufil 19441

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 2418 ax-rep 4396 ax-sep 4406 ax-nul 4414 ax-pow 4463 ax-pr 4524 ax-un 6367 ax-ac2 8624

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 2256 df-mo 2257 df-clab 2424 df-cleq 2430 df-clel 2433 df-nfc 2562 df-ne 2602 df-nel 2603 df-ral 2714 df-rex 2715 df-reu 2716 df-rmo 2717 df-rab 2718 df-v 2968 df-sbc 3180 df-csb 3282 df-dif 3324 df-un 3326 df-in 3328 df-ss 3335 df-pss 3337 df-nul 3631 df-if 3785 df-pw 3855 df-sn 3871 df-pr 3873 df-tp 3875 df-op 3877 df-uni 4085 df-int 4122 df-iun 4166 df-br 4286 df-opab 4344 df-mpt 4345 df-tr 4379 df-eprel 4624 df-id 4628 df-po 4633 df-so 4634 df-fr 4671 df-se 4672 df-we 4673 df-ord 4714 df-on 4715 df-lim 4716 df-suc 4717 df-xp 4838 df-rel 4839 df-cnv 4840 df-co 4841 df-dm 4842 df-rn 4843 df-res 4844 df-ima 4845 df-iota 5374 df-fun 5413 df-fn 5414 df-f 5415 df-f1 5416 df-fo 5417 df-f1o 5418 df-fv 5419 df-isom 5420 df-riota 6045 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-rpss 6355 df-om 6472 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-en 7303 df-dom 7304 df-fin 7306 df-fi 7653 df-card 8101 df-ac 8278 df-cda 8329 df-fbas 17783 df-fg 17784 df-fil 19388 df-ufil 19443

This theorem is referenced by: (None)

W3C validator