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

Metamath Proof Explorer

Theorem filufint

Proof