filufint

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)

		Ref	Expression
	Assertion	filufint	$⊢ F \in Fil (X) \to ⋂ \{f \in UFil (X) \| F \subseteq f\} = F$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	elintrab	$⊢ x \in ⋂ \{f \in UFil (X) \| F \subseteq f\} \leftrightarrow \forall f \in UFil (X) (F \subseteq f \to x \in f)$
3		filsspw	$⊢ F \in Fil (X) \to F \subseteq 𝒫 X$
4	3	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to F \subseteq 𝒫 X$
5		difss	$⊢ X ∖ x \subseteq X$
6		filtop	$⊢ F \in Fil (X) \to X \in F$
7		difexg	$⊢ X \in F \to X ∖ x \in V$
8	6 7	syl	$⊢ F \in Fil (X) \to X ∖ x \in V$
9	8	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to X ∖ x \in V$
10		elpwg	$⊢ X ∖ x \in V \to (X ∖ x \in 𝒫 X \leftrightarrow X ∖ x \subseteq X)$
11	9 10	syl	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to (X ∖ x \in 𝒫 X \leftrightarrow X ∖ x \subseteq X)$
12	5 11	mpbiri	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to X ∖ x \in 𝒫 X$
13	12	snssd	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to \{X ∖ x\} \subseteq 𝒫 X$
14	4 13	unssd	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to F \cup \{X ∖ x\} \subseteq 𝒫 X$
15		ssun1	$⊢ F \subseteq F \cup \{X ∖ x\}$
16		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
17		ssn0	$⊢ (F \subseteq F \cup \{X ∖ x\} \land F \neq \emptyset) \to F \cup \{X ∖ x\} \neq \emptyset$
18	15 16 17	sylancr	$⊢ F \in Fil (X) \to F \cup \{X ∖ x\} \neq \emptyset$
19	18	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to F \cup \{X ∖ x\} \neq \emptyset$
20		elsni	$⊢ z \in \{X ∖ x\} \to z = X ∖ x$
21		filelss	$⊢ (F \in Fil (X) \land y \in F) \to y \subseteq X$
22	21	3adant3	$⊢ (F \in Fil (X) \land y \in F \land x \subseteq X) \to y \subseteq X$
23		reldisj	$⊢ y \subseteq X \to (y \cap (X ∖ x) = \emptyset \leftrightarrow y \subseteq X ∖ (X ∖ x))$
24	22 23	syl	$⊢ (F \in Fil (X) \land y \in F \land x \subseteq X) \to (y \cap (X ∖ x) = \emptyset \leftrightarrow y \subseteq X ∖ (X ∖ x))$
25		dfss4	$⊢ x \subseteq X \leftrightarrow X ∖ (X ∖ x) = x$
26	25	biimpi	$⊢ x \subseteq X \to X ∖ (X ∖ x) = x$
27	26	sseq2d	$⊢ x \subseteq X \to (y \subseteq X ∖ (X ∖ x) \leftrightarrow y \subseteq x)$
28	27	3ad2ant3	$⊢ (F \in Fil (X) \land y \in F \land x \subseteq X) \to (y \subseteq X ∖ (X ∖ x) \leftrightarrow y \subseteq x)$
29	24 28	bitrd	$⊢ (F \in Fil (X) \land y \in F \land x \subseteq X) \to (y \cap (X ∖ x) = \emptyset \leftrightarrow y \subseteq x)$
30		filss	$⊢ (F \in Fil (X) \land (y \in F \land x \subseteq X \land y \subseteq x)) \to x \in F$
31	30	3exp2	$⊢ F \in Fil (X) \to (y \in F \to (x \subseteq X \to (y \subseteq x \to x \in F)))$
32	31	3imp	$⊢ (F \in Fil (X) \land y \in F \land x \subseteq X) \to (y \subseteq x \to x \in F)$
33	29 32	sylbid	$⊢ (F \in Fil (X) \land y \in F \land x \subseteq X) \to (y \cap (X ∖ x) = \emptyset \to x \in F)$
34	33	necon3bd	$⊢ (F \in Fil (X) \land y \in F \land x \subseteq X) \to (\neg x \in F \to y \cap (X ∖ x) \neq \emptyset)$
35	34	3exp	$⊢ F \in Fil (X) \to (y \in F \to (x \subseteq X \to (\neg x \in F \to y \cap (X ∖ x) \neq \emptyset)))$
36	35	com24	$⊢ F \in Fil (X) \to (\neg x \in F \to (x \subseteq X \to (y \in F \to y \cap (X ∖ x) \neq \emptyset)))$
37	36	3imp1	$⊢ ((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land y \in F) \to y \cap (X ∖ x) \neq \emptyset$
38		ineq2	$⊢ z = X ∖ x \to y \cap z = y \cap (X ∖ x)$
39	38	neeq1d	$⊢ z = X ∖ x \to (y \cap z \neq \emptyset \leftrightarrow y \cap (X ∖ x) \neq \emptyset)$
40	37 39	syl5ibrcom	$⊢ ((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land y \in F) \to (z = X ∖ x \to y \cap z \neq \emptyset)$
41	40	expimpd	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to ((y \in F \land z = X ∖ x) \to y \cap z \neq \emptyset)$
42	20 41	sylan2i	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to ((y \in F \land z \in \{X ∖ x\}) \to y \cap z \neq \emptyset)$
43	42	ralrimivv	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to \forall y \in F \forall z \in \{X ∖ x\} y \cap z \neq \emptyset$
44		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
45	44	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to F \in fBas (X)$
46	5	a1i	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to X ∖ x \subseteq X$
47	26	3ad2ant2	$⊢ (F \in Fil (X) \land x \subseteq X \land X ∖ x = \emptyset) \to X ∖ (X ∖ x) = x$
48		difeq2	$⊢ X ∖ x = \emptyset \to X ∖ (X ∖ x) = X ∖ \emptyset$
49		dif0	$⊢ X ∖ \emptyset = X$
50	48 49	syl6eq	$⊢ X ∖ x = \emptyset \to X ∖ (X ∖ x) = X$
51	50	3ad2ant3	$⊢ (F \in Fil (X) \land x \subseteq X \land X ∖ x = \emptyset) \to X ∖ (X ∖ x) = X$
52	47 51	eqtr3d	$⊢ (F \in Fil (X) \land x \subseteq X \land X ∖ x = \emptyset) \to x = X$
53	6	3ad2ant1	$⊢ (F \in Fil (X) \land x \subseteq X \land X ∖ x = \emptyset) \to X \in F$
54	52 53	eqeltrd	$⊢ (F \in Fil (X) \land x \subseteq X \land X ∖ x = \emptyset) \to x \in F$
55	54	3expia	$⊢ (F \in Fil (X) \land x \subseteq X) \to (X ∖ x = \emptyset \to x \in F)$
56	55	necon3bd	$⊢ (F \in Fil (X) \land x \subseteq X) \to (\neg x \in F \to X ∖ x \neq \emptyset)$
57	56	ex	$⊢ F \in Fil (X) \to (x \subseteq X \to (\neg x \in F \to X ∖ x \neq \emptyset))$
58	57	com23	$⊢ F \in Fil (X) \to (\neg x \in F \to (x \subseteq X \to X ∖ x \neq \emptyset))$
59	58	3imp	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to X ∖ x \neq \emptyset$
60	6	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to X \in F$
61		snfbas	$⊢ (X ∖ x \subseteq X \land X ∖ x \neq \emptyset \land X \in F) \to \{X ∖ x\} \in fBas (X)$
62	46 59 60 61	syl3anc	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to \{X ∖ x\} \in fBas (X)$
63		fbunfip	$⊢ (F \in fBas (X) \land \{X ∖ x\} \in fBas (X)) \to (\neg \emptyset \in fi (F \cup \{X ∖ x\}) \leftrightarrow \forall y \in F \forall z \in \{X ∖ x\} y \cap z \neq \emptyset)$
64	45 62 63	syl2anc	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to (\neg \emptyset \in fi (F \cup \{X ∖ x\}) \leftrightarrow \forall y \in F \forall z \in \{X ∖ x\} y \cap z \neq \emptyset)$
65	43 64	mpbird	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to \neg \emptyset \in fi (F \cup \{X ∖ x\})$
66		fsubbas	$⊢ X \in F \to (fi (F \cup \{X ∖ x\}) \in fBas (X) \leftrightarrow (F \cup \{X ∖ x\} \subseteq 𝒫 X \land F \cup \{X ∖ x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{X ∖ x\})))$
67	6 66	syl	$⊢ F \in Fil (X) \to (fi (F \cup \{X ∖ x\}) \in fBas (X) \leftrightarrow (F \cup \{X ∖ x\} \subseteq 𝒫 X \land F \cup \{X ∖ x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{X ∖ x\})))$
68	67	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to (fi (F \cup \{X ∖ x\}) \in fBas (X) \leftrightarrow (F \cup \{X ∖ x\} \subseteq 𝒫 X \land F \cup \{X ∖ x\} \neq \emptyset \land \neg \emptyset \in fi (F \cup \{X ∖ x\})))$
69	14 19 65 68	mpbir3and	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to fi (F \cup \{X ∖ x\}) \in fBas (X)$
70		fgcl	$⊢ fi (F \cup \{X ∖ x\}) \in fBas (X) \to X filGen fi (F \cup \{X ∖ x\}) \in Fil (X)$
71	69 70	syl	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to X filGen fi (F \cup \{X ∖ x\}) \in Fil (X)$
72		filssufil	$⊢ X filGen fi (F \cup \{X ∖ x\}) \in Fil (X) \to \exists f \in UFil (X) X filGen fi (F \cup \{X ∖ x\}) \subseteq f$
73		snex	$⊢ \{X ∖ x\} \in V$
74		unexg	$⊢ (F \in Fil (X) \land \{X ∖ x\} \in V) \to F \cup \{X ∖ x\} \in V$
75	73 74	mpan2	$⊢ F \in Fil (X) \to F \cup \{X ∖ x\} \in V$
76		ssfii	$⊢ F \cup \{X ∖ x\} \in V \to F \cup \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
77	75 76	syl	$⊢ F \in Fil (X) \to F \cup \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
78	77	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to F \cup \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
79	78	unssad	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to F \subseteq fi (F \cup \{X ∖ x\})$
80		ssfg	$⊢ fi (F \cup \{X ∖ x\}) \in fBas (X) \to fi (F \cup \{X ∖ x\}) \subseteq X filGen fi (F \cup \{X ∖ x\})$
81	69 80	syl	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to fi (F \cup \{X ∖ x\}) \subseteq X filGen fi (F \cup \{X ∖ x\})$
82	79 81	sstrd	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to F \subseteq X filGen fi (F \cup \{X ∖ x\})$
83	82	ad2antrr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to F \subseteq X filGen fi (F \cup \{X ∖ x\})$
84		simpr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq f$
85	83 84	sstrd	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to F \subseteq f$
86		ufilfil	$⊢ f \in UFil (X) \to f \in Fil (X)$
87		0nelfil	$⊢ f \in Fil (X) \to \neg \emptyset \in f$
88	86 87	syl	$⊢ f \in UFil (X) \to \neg \emptyset \in f$
89	88	ad2antlr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to \neg \emptyset \in f$
90		disjdif	$⊢ x \cap (X ∖ x) = \emptyset$
91	86	ad2antlr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to f \in Fil (X)$
92		simprr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to x \in f$
93	77	unssbd	$⊢ F \in Fil (X) \to \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
94	93	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
95	94	adantr	$⊢ ((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \to \{X ∖ x\} \subseteq fi (F \cup \{X ∖ x\})$
96	69	adantr	$⊢ ((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \to fi (F \cup \{X ∖ x\}) \in fBas (X)$
97	96 80	syl	$⊢ ((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \to fi (F \cup \{X ∖ x\}) \subseteq X filGen fi (F \cup \{X ∖ x\})$
98	95 97	sstrd	$⊢ ((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \to \{X ∖ x\} \subseteq X filGen fi (F \cup \{X ∖ x\})$
99	98	adantr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to \{X ∖ x\} \subseteq X filGen fi (F \cup \{X ∖ x\})$
100		simprl	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to X filGen fi (F \cup \{X ∖ x\}) \subseteq f$
101	99 100	sstrd	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to \{X ∖ x\} \subseteq f$
102		snidg	$⊢ X ∖ x \in V \to X ∖ x \in \{X ∖ x\}$
103	8 102	syl	$⊢ F \in Fil (X) \to X ∖ x \in \{X ∖ x\}$
104	103	3ad2ant1	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to X ∖ x \in \{X ∖ x\}$
105	104	ad2antrr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to X ∖ x \in \{X ∖ x\}$
106	101 105	sseldd	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to X ∖ x \in f$
107		filin	$⊢ (f \in Fil (X) \land x \in f \land X ∖ x \in f) \to x \cap (X ∖ x) \in f$
108	91 92 106 107	syl3anc	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to x \cap (X ∖ x) \in f$
109	90 108	eqeltrrid	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \land x \in f)) \to \emptyset \in f$
110	109	expr	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to (x \in f \to \emptyset \in f)$
111	89 110	mtod	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to \neg x \in f$
112	85 111	jca	$⊢ (((F \in Fil (X) \land \neg x \in F \land x \subseteq X) \land f \in UFil (X)) \land X filGen fi (F \cup \{X ∖ x\}) \subseteq f) \to (F \subseteq f \land \neg x \in f)$
113	112	exp31	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to (f \in UFil (X) \to (X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to (F \subseteq f \land \neg x \in f)))$
114	113	reximdvai	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to (\exists f \in UFil (X) X filGen fi (F \cup \{X ∖ x\}) \subseteq f \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f))$
115	72 114	syl5	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to (X filGen fi (F \cup \{X ∖ x\}) \in Fil (X) \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f))$
116	71 115	mpd	$⊢ (F \in Fil (X) \land \neg x \in F \land x \subseteq X) \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f)$
117	116	3expia	$⊢ (F \in Fil (X) \land \neg x \in F) \to (x \subseteq X \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f))$
118		filssufil	$⊢ F \in Fil (X) \to \exists f \in UFil (X) F \subseteq f$
119		filelss	$⊢ (f \in Fil (X) \land x \in f) \to x \subseteq X$
120	119	ex	$⊢ f \in Fil (X) \to (x \in f \to x \subseteq X)$
121	86 120	syl	$⊢ f \in UFil (X) \to (x \in f \to x \subseteq X)$
122	121	con3d	$⊢ f \in UFil (X) \to (\neg x \subseteq X \to \neg x \in f)$
123	122	impcom	$⊢ (\neg x \subseteq X \land f \in UFil (X)) \to \neg x \in f$
124	123	a1d	$⊢ (\neg x \subseteq X \land f \in UFil (X)) \to (F \subseteq f \to \neg x \in f)$
125	124	ancld	$⊢ (\neg x \subseteq X \land f \in UFil (X)) \to (F \subseteq f \to (F \subseteq f \land \neg x \in f))$
126	125	reximdva	$⊢ \neg x \subseteq X \to (\exists f \in UFil (X) F \subseteq f \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f))$
127	118 126	syl5com	$⊢ F \in Fil (X) \to (\neg x \subseteq X \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f))$
128	127	adantr	$⊢ (F \in Fil (X) \land \neg x \in F) \to (\neg x \subseteq X \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f))$
129	117 128	pm2.61d	$⊢ (F \in Fil (X) \land \neg x \in F) \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f)$
130	129	ex	$⊢ F \in Fil (X) \to (\neg x \in F \to \exists f \in UFil (X) (F \subseteq f \land \neg x \in f))$
131		rexanali	$⊢ \exists f \in UFil (X) (F \subseteq f \land \neg x \in f) \leftrightarrow \neg \forall f \in UFil (X) (F \subseteq f \to x \in f)$
132	130 131	syl6ib	$⊢ F \in Fil (X) \to (\neg x \in F \to \neg \forall f \in UFil (X) (F \subseteq f \to x \in f))$
133	132	con4d	$⊢ F \in Fil (X) \to (\forall f \in UFil (X) (F \subseteq f \to x \in f) \to x \in F)$
134	2 133	syl5bi	$⊢ F \in Fil (X) \to (x \in ⋂ \{f \in UFil (X) \| F \subseteq f\} \to x \in F)$
135	134	ssrdv	$⊢ F \in Fil (X) \to ⋂ \{f \in UFil (X) \| F \subseteq f\} \subseteq F$
136		ssintub	$⊢ F \subseteq ⋂ \{f \in UFil (X) \| F \subseteq f\}$
137	136	a1i	$⊢ F \in Fil (X) \to F \subseteq ⋂ \{f \in UFil (X) \| F \subseteq f\}$
138	135 137	eqssd	$⊢ F \in Fil (X) \to ⋂ \{f \in UFil (X) \| F \subseteq f\} = F$

Metamath Proof Explorer

Theorem filufint

Proof