filufint - Metamath Proof Explorer

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

Theorem filufint 20506

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 3037	. . . . 5
2	1	elintrab 4211	. . . 4
3		filsspw 20437	. . . . . . . . . . . . . 14
4	3	3ad2ant1 1015	. . . . . . . . . . . . 13 $/\$ $/\$
5		difss 3545	. . . . . . . . . . . . . . 15 $\$
6		filtop 20441	. . . . . . . . . . . . . . . . . 18
7		difexg 4513	. . . . . . . . . . . . . . . . . 18 $\$
8	6, 7	syl 16	. . . . . . . . . . . . . . . . 17 $\$
9	8	3ad2ant1 1015	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
10		elpwg 3935	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
11	9, 10	syl 16	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
12	5, 11	mpbiri 233	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
13	12	snssd 4089	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
14	4, 13	unssd 3594	. . . . . . . . . . . 12 $/\$ $/\$ $\$
15		ssun1 3581	. . . . . . . . . . . . . 14 $\$
16		filn0 20448	. . . . . . . . . . . . . 14
17		ssn0 3745	. . . . . . . . . . . . . 14 $\$ $/\$ $\$
18	15, 16, 17	sylancr 661	. . . . . . . . . . . . 13 $\$
19	18	3ad2ant1 1015	. . . . . . . . . . . 12 $/\$ $/\$ $\$
20		elsni 3969	. . . . . . . . . . . . . . 15 $\$ $\$
21		filelss 20438	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	21	3adant3 1014	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23		reldisj 3786	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
24	22, 23	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$ $\$
25		dfss4 3657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $\$
26	25	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$
27	26	sseq2d 3445	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
28	27	3ad2ant3 1017	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
29	24, 28	bitrd 253	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
30		filss 20439	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
31	30	3exp2 1212	. . . . . . . . . . . . . . . . . . . . . . 23
32	31	3imp 1188	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
33	29, 32	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
34	33	necon3bd 2594	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
35	34	3exp 1193	. . . . . . . . . . . . . . . . . . 19 $\$
36	35	com24 87	. . . . . . . . . . . . . . . . . 18 $\$
37	36	3imp1 1207	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $\$
38		ineq2 3608	. . . . . . . . . . . . . . . . . 18 $\$ $\$
39	38	neeq1d 2659	. . . . . . . . . . . . . . . . 17 $\$ $\$
40	37, 39	syl5ibrcom 222	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $\$
41	40	expimpd 601	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $\$
42	20, 41	sylan2i 653	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
43	42	ralrimivv 2802	. . . . . . . . . . . . 13 $/\$ $/\$ $\$
44		filfbas 20434	. . . . . . . . . . . . . . 15
45	44	3ad2ant1 1015	. . . . . . . . . . . . . 14 $/\$ $/\$
46	5	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
47	26	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
48		difeq2 3530	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$ $\$
49		dif0 3814	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
50	48, 49	syl6eq 2439	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
51	50	3ad2ant3 1017	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$ $\$ $\$
52	47, 51	eqtr3d 2425	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
53	6	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
54	52, 53	eqeltrd 2470	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$
55	54	3expia 1196	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
56	55	necon3bd 2594	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
57	56	ex 432	. . . . . . . . . . . . . . . . 17 $\$
58	57	com23 78	. . . . . . . . . . . . . . . 16 $\$
59	58	3imp 1188	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
60	6	3ad2ant1 1015	. . . . . . . . . . . . . . 15 $/\$ $/\$
61		snfbas 20452	. . . . . . . . . . . . . . 15 $\$ $/\$ $\$ $/\$ $\$
62	46, 59, 60, 61	syl3anc 1226	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$
63		fbunfip 20455	. . . . . . . . . . . . . 14 $/\$ $\$ $\$ $\$
64	45, 62, 63	syl2anc 659	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
65	43, 64	mpbird 232	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66		fsubbas 20453	. . . . . . . . . . . . . 14 $\$ $\$ $/\$ $\$ $/\$ $\$
67	6, 66	syl 16	. . . . . . . . . . . . 13 $\$ $\$ $/\$ $\$ $/\$ $\$
68	67	3ad2ant1 1015	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$ $/\$ $\$ $/\$ $\$
69	14, 19, 65, 68	mpbir3and 1177	. . . . . . . . . . 11 $/\$ $/\$ $\$
70		fgcl 20464	. . . . . . . . . . 11 $\$ $\$
71	69, 70	syl 16	. . . . . . . . . 10 $/\$ $/\$ $\$
72		filssufil 20498	. . . . . . . . . . 11 $\$ $\$
73		snex 4603	. . . . . . . . . . . . . . . . . . . . 21 $\$
74		unexg 6500	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$ $\$
75	73, 74	mpan2 669	. . . . . . . . . . . . . . . . . . . 20 $\$
76		ssfii 7794	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
77	75, 76	syl 16	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
78	77	3ad2ant1 1015	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
79	78	unssad 3595	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$
80		ssfg 20458	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
81	69, 80	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
82	79, 81	sstrd 3427	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$
83	82	ad2antrr 723	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
84		simpr 459	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$ $\$
85	83, 84	sstrd 3427	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
86		ufilfil 20490	. . . . . . . . . . . . . . . . 17
87		0nelfil 20435	. . . . . . . . . . . . . . . . 17
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16
89	88	ad2antlr 724	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
90		disjdif 3816	. . . . . . . . . . . . . . . . 17 $\$
91	86	ad2antlr 724	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
92		simprr 755	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
93	77	unssbd 3596	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$
94	93	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$ $\$
95	94	adantr 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
96	69	adantr 463	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
97	96, 80	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$ $\$
98	95, 97	sstrd 3427	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$ $\$
99	98	adantr 463	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
100		simprl 754	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
101	99, 100	sstrd 3427	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
102		snidg 3970	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
103	8, 102	syl 16	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
104	103	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\$ $\$
105	104	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$ $\$
106	101, 105	sseldd 3418	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
107		filin 20440	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $\$ $\$
108	91, 92, 106, 107	syl3anc 1226	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $\$ $/\$ $\$
109	90, 108	syl5eqelr 2475	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
110	109	expr 613	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $\$
111	89, 110	mtod 177	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $\$
112	85, 111	jca 530	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$ $/\$
113	112	exp31 602	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $/\$
114	113	reximdvai 2854	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$
115	72, 114	syl5 32	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
116	71, 115	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$
117	116	3expia 1196	. . . . . . . 8 $/\$ $/\$
118		filssufil 20498	. . . . . . . . . 10
119		filelss 20438	. . . . . . . . . . . . . . . . 17 $/\$
120	119	ex 432	. . . . . . . . . . . . . . . 16
121	86, 120	syl 16	. . . . . . . . . . . . . . 15
122	121	con3d 133	. . . . . . . . . . . . . 14
123	122	impcom 428	. . . . . . . . . . . . 13 $/\$
124	123	a1d 25	. . . . . . . . . . . 12 $/\$
125	124	ancld 551	. . . . . . . . . . 11 $/\$ $/\$
126	125	reximdva 2857	. . . . . . . . . 10 $/\$
127	118, 126	syl5com 30	. . . . . . . . 9 $/\$
128	127	adantr 463	. . . . . . . 8 $/\$ $/\$
129	117, 128	pm2.61d 158	. . . . . . 7 $/\$ $/\$
130	129	ex 432	. . . . . 6 $/\$
131		rexanali 2835	. . . . . 6 $/\$
132	130, 131	syl6ib 226	. . . . 5
133	132	con4d 105	. . . 4
134	2, 133	syl5bi 217	. . 3
135	134	ssrdv 3423	. 2
136		ssintub 4217	. . 3
137	136	a1i 11	. 2
138	135, 137	eqssd 3434	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1826

wne 2577

wral 2732

wrex 2733

crab 2736

cvv 3034 $\$ cdif 3386

cun 3387

cin 3388

wss 3389

c0 3711

cpw 3927

csn 3944

cint 4199

cfv 5496 (class class class)co 6196

cfi 7785

cfbas 18519

cfg 18520

cfil 20431

cufil 20485

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-ac2 8756

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-rpss 6479 df-om 6600 df-recs 6960 df-rdg 6994 df-1o 7048 df-oadd 7052 df-er 7229 df-en 7436 df-dom 7437 df-fin 7439 df-fi 7786 df-card 8233 df-ac 8410 df-cda 8461 df-fbas 18529 df-fg 18530 df-fil 20432 df-ufil 20487

This theorem is referenced by: (None)

W3C validator