P. 235 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23401-23500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fgtr 23401	If 𝐴 is a member of the filter, then truncating 𝐹 to 𝐴 and regenerating the behavior outside 𝐴 using filGen recovers the original filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑋filGen(𝐹 ↾t 𝐴)) = 𝐹)
Theorem	trfg 23402	The trace operation and the filGen operation are inverses to one another in some sense, with filGen growing the base set and ↾t shrinking it. See fgtr 23401 for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐹 ∈ (Fil‘𝐴) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉) → ((𝑋filGen𝐹) ↾t 𝐴) = 𝐹)
Theorem	trnei 23403	The trace, over a set 𝐴, of the filter of the neighborhoods of a point 𝑃 is a filter iff 𝑃 belongs to the closure of 𝐴. (This is trfil2 23398 applied to a filter of neighborhoods.) (Contributed by FL, 15-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌) → (𝑃 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑃}) ↾t 𝐴) ∈ (Fil‘𝐴)))
Theorem	cfinfil 23404*	Relative complements of the finite parts of an infinite set is a filter. When 𝐴 = ℕ the set of the relative complements is called Frechet's filter and is used to define the concept of limit of a sequence. (Contributed by FL, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∖ 𝑥) ∈ Fin} ∈ (Fil‘𝑋))
Theorem	csdfil 23405*	The set of all elements whose complement is dominated by the base set is a filter. (Contributed by Mario Carneiro, 14-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝑋 ∈ dom card ∧ ω ≼ 𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ≺ 𝑋} ∈ (Fil‘𝑋))
Theorem	supfil 23406*	The supersets of a nonempty set which are also subsets of a given base set form a filter. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → {𝑥 ∈ 𝒫 𝐴 ∣ 𝐵 ⊆ 𝑥} ∈ (Fil‘𝐴))
Theorem	zfbas 23407	The set of upper sets of integers is a filter base on ℤ, which corresponds to convergence of sequences on ℤ. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ran ℤ≥ ∈ (fBas‘ℤ)
Theorem	uzrest 23408	The restriction of the set of upper sets of integers to an upper set of integers is the set of upper sets of integers based at a point above the cutoff. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → (ran ℤ≥ ↾t 𝑍) = (ℤ≥ “ 𝑍))
Theorem	uzfbas 23409	The set of upper sets of integers based at a point in a fixed upper integer set like ℕ is a filter base on ℕ, which corresponds to convergence of sequences on ℕ. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ (𝑀 ∈ ℤ → (ℤ≥ “ 𝑍) ∈ (fBas‘𝑍))
12.2.3  Ultrafilters
Syntax	cufil 23410	Extend class notation with the ultrafilters-on-a-set function.
class UFil
Syntax	cufl 23411	Extend class notation with the ultrafilter lemma.
class UFL
Definition	df-ufil 23412*	Define the set of ultrafilters on a set. An ultrafilter is a filter that gives a definite result for every subset. (Contributed by Jeff Hankins, 30-Nov-2009.)
⊢ UFil = (𝑔 ∈ V ↦ {𝑓 ∈ (Fil‘𝑔) ∣ ∀𝑥 ∈ 𝒫 𝑔(𝑥 ∈ 𝑓 ∨ (𝑔 ∖ 𝑥) ∈ 𝑓)})
Definition	df-ufl 23413*	Define the class of base sets for which the ultrafilter lemma filssufil 23423 holds. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ UFL = {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔}
Theorem	isufil 23414*	The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)))
Theorem	ufilfil 23415	An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
Theorem	ufilss 23416	For any subset of the base set of an ultrafilter, either the set is in the ultrafilter or the complement is. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐹 ∨ (𝑋 ∖ 𝑆) ∈ 𝐹))
Theorem	ufilb 23417	The complement is in an ultrafilter iff the set is not. (Contributed by Mario Carneiro, 11-Dec-2013.) (Revised by Mario Carneiro, 29-Jul-2015.)
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (¬ 𝑆 ∈ 𝐹 ↔ (𝑋 ∖ 𝑆) ∈ 𝐹))
Theorem	ufilmax 23418	Any filter finer than an ultrafilter is actually equal to it. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → 𝐹 = 𝐺)
Theorem	isufil2 23419*	The maximal property of an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑓 → 𝐹 = 𝑓)))
Theorem	ufprim 23420	An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Mario Carneiro, 2-Aug-2015.)
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((𝐴 ∈ 𝐹 ∨ 𝐵 ∈ 𝐹) ↔ (𝐴 ∪ 𝐵) ∈ 𝐹))
Theorem	trufil 23421	Conditions for the trace of an ultrafilter 𝐿 to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((𝐿 ∈ (UFil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (UFil‘𝐴) ↔ 𝐴 ∈ 𝐿))
Theorem	filssufilg 23422*	A filter is contained in some ultrafilter. This version of filssufil 23423 contains the choice as a hypothesis (in the assumption that 𝒫 𝒫 𝑋 is well-orderable). (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝒫 𝒫 𝑋 ∈ dom card) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
Theorem	filssufil 23423*	A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 10467.) (Contributed by Jeff Hankins, 2-Dec-2009.) (Revised by Stefan O'Rear, 29-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
Theorem	isufl 23424*	Define the (strong) ultrafilter lemma, parameterized over base sets. A set 𝑋 satisfies the ultrafilter lemma if every filter on 𝑋 is a subset of some ultrafilter. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑋 ∈ 𝑉 → (𝑋 ∈ UFL ↔ ∀𝑓 ∈ (Fil‘𝑋)∃𝑔 ∈ (UFil‘𝑋)𝑓 ⊆ 𝑔))
Theorem	ufli 23425*	Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝑋 ∈ UFL ∧ 𝐹 ∈ (Fil‘𝑋)) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
Theorem	numufl 23426	Consequence of filssufilg 23422: a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL)
Theorem	fiufl 23427	A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑋 ∈ Fin → 𝑋 ∈ UFL)
Theorem	acufl 23428	The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (CHOICE → UFL = V)
Theorem	ssufl 23429	If 𝑌 is a subset of 𝑋 and filters extend to ultrafilters in 𝑋, then they still do in 𝑌. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝑋 ∈ UFL ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ UFL)
Theorem	ufileu 23430*	If the ultrafilter containing a given filter is unique, the filter is an ultrafilter. (Contributed by Jeff Hankins, 3-Dec-2009.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∈ (UFil‘𝑋) ↔ ∃!𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓))
Theorem	filufint 23431*	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.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ∩ {𝑓 ∈ (UFil‘𝑋) ∣ 𝐹 ⊆ 𝑓} = 𝐹)
Theorem	uffix 23432*	Lemma for fixufil 23433 and uffixfr 23434. (Contributed by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → ({{𝐴}} ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} = (𝑋filGen{{𝐴}})))
Theorem	fixufil 23433*	The condition describing a fixed ultrafilter always produces an ultrafilter. (Contributed by Jeff Hankins, 9-Dec-2009.) (Revised by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 29-Jul-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} ∈ (UFil‘𝑋))
Theorem	uffixfr 23434*	An ultrafilter is either fixed or free. A fixed ultrafilter is called principal (generated by a single element 𝐴), and a free ultrafilter is called nonprincipal (having empty intersection). Note that examples of free ultrafilters cannot be defined in ZFC without some form of global choice. (Contributed by Jeff Hankins, 4-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐴 ∈ ∩ 𝐹 ↔ 𝐹 = {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥}))
Theorem	uffix2 23435*	A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 ≠ ∅ ↔ ∃𝑥 ∈ 𝑋 𝐹 = {𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦}))
Theorem	uffixsn 23436	The singleton of the generator of a fixed ultrafilter is in the filter. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐴 ∈ ∩ 𝐹) → {𝐴} ∈ 𝐹)
Theorem	ufildom1 23437	An ultrafilter is generated by at most one element (because free ultrafilters have no generators and fixed ultrafilters have exactly one). (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → ∩ 𝐹 ≼ 1o)
Theorem	uffinfix 23438*	An ultrafilter containing a finite element is fixed. (Contributed by Jeff Hankins, 5-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝑆 ∈ Fin) → ∃𝑥 ∈ 𝑋 𝐹 = {𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦})
Theorem	cfinufil 23439*	An ultrafilter is free iff it contains the Fréchet filter cfinfil 23404 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 = ∅ ↔ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹))
Theorem	ufinffr 23440*	An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Mario Carneiro, 4-Dec-2013.)
⊢ ((𝑋 ∈ 𝐵 ∧ 𝐴 ⊆ 𝑋 ∧ ω ≼ 𝐴) → ∃𝑓 ∈ (UFil‘𝑋)(𝐴 ∈ 𝑓 ∧ ∩ 𝑓 = ∅))
Theorem	ufilen 23441*	Any infinite set has an ultrafilter on it whose elements are of the same cardinality as the set. Any such ultrafilter is necessarily free. (Contributed by Jeff Hankins, 7-Dec-2009.) (Revised by Stefan O'Rear, 3-Aug-2015.)
⊢ (ω ≼ 𝑋 → ∃𝑓 ∈ (UFil‘𝑋)∀𝑥 ∈ 𝑓 𝑥 ≈ 𝑋)
Theorem	ufildr 23442	An ultrafilter gives rise to a connected door topology. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Stefan O'Rear, 3-Aug-2015.)
⊢ 𝐽 = (𝐹 ∪ {∅})    ⇒   ⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 ∪ (Clsd‘𝐽)) = 𝒫 𝑋)
Theorem	fin1aufil 23443	There are no definable free ultrafilters in ZFC. However, there are free ultrafilters in some choice-denying constructions. Here we show that given an amorphous set (a.k.a. a Ia-finite I-infinite set) 𝑋, the set of infinite subsets of 𝑋 is a free ultrafilter on 𝑋. (Contributed by Mario Carneiro, 20-May-2015.)
⊢ 𝐹 = (𝒫 𝑋 ∖ Fin)    ⇒   ⊢ (𝑋 ∈ (FinIa ∖ Fin) → (𝐹 ∈ (UFil‘𝑋) ∧ ∩ 𝐹 = ∅))
12.2.4  Filter limits
Syntax	cfm 23444	Extend class definition to include the neighborhood filter mapping function.
class FilMap
Syntax	cflim 23445	Extend class notation with a function returning the limit of a filter.
class fLim
Syntax	cflf 23446	Extend class definition to include the function for filter-based function limits.
class fLimf
Syntax	cfcls 23447	Extend class definition to include the cluster point function on filters.
class fClus
Syntax	cfcf 23448	Extend class definition to include the function for cluster points of a function.
class fClusf
Definition	df-fm 23449*	Define a function that takes a filter to a neighborhood filter of the range. (Since we now allow filter bases to have support smaller than the base set, the function has to come first to ensure that curryings are sets.) (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 20-Jul-2015.)
⊢ FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑦 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑡 ∈ 𝑦 ↦ (𝑓 “ 𝑡)))))
Definition	df-flim 23450*	Define a function (indexed by a topology 𝑗) whose value is the limits of a filter 𝑓. (Contributed by Jeff Hankins, 4-Sep-2009.)
⊢ fLim = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ {𝑥 ∈ ∪ 𝑗 ∣ (((nei‘𝑗)‘{𝑥}) ⊆ 𝑓 ∧ 𝑓 ⊆ 𝒫 ∪ 𝑗)})
Definition	df-flf 23451*	Define a function that gives the limits of a function 𝑓 in the filter sense. (Contributed by Jeff Hankins, 14-Oct-2009.)
⊢ fLimf = (𝑥 ∈ Top, 𝑦 ∈ ∪ ran Fil ↦ (𝑓 ∈ (∪ 𝑥 ↑m ∪ 𝑦) ↦ (𝑥 fLim ((∪ 𝑥 FilMap 𝑓)‘𝑦))))
Definition	df-fcls 23452*	Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009.)
⊢ fClus = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ if(∪ 𝑗 = ∪ 𝑓, ∩ 𝑥 ∈ 𝑓 ((cls‘𝑗)‘𝑥), ∅))
Definition	df-fcf 23453*	Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.)
⊢ fClusf = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑m ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))
Theorem	fmval 23454*	Introduce a function that takes a function from a filtered domain to a set and produces a filter which consists of supersets of images of filter elements. The functions which are dealt with by this function are similar to nets in topology. For example, suppose we have a sequence filtered by the filter generated by its tails under the usual positive integer ordering. Then the elements of this filter are precisely the supersets of tails of this sequence. Under this definition, it is not too difficult to see that the limit of a function in the filter sense captures the notion of convergence of a sequence. As a result, the notion of a filter generalizes many ideas associated with sequences, and this function is one way to make that relationship precise in Metamath. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))
Theorem	fmfil 23455	A mapping filter is a filter. (Contributed by Jeff Hankins, 18-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) ∈ (Fil‘𝑋))
Theorem	fmf 23456	Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
Theorem	fmss 23457	A finer filter produces a finer image filter. (Contributed by Jeff Hankins, 16-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ (((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐶 ∈ (fBas‘𝑌)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐵 ⊆ 𝐶)) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ ((𝑋 FilMap 𝐹)‘𝐶))
Theorem	elfm 23458*	An element of a mapping filter. (Contributed by Jeff Hankins, 8-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ ((𝑋 ∈ 𝐶 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴 ⊆ 𝑋 ∧ ∃𝑥 ∈ 𝐵 (𝐹 “ 𝑥) ⊆ 𝐴)))
Theorem	elfm2 23459*	An element of a mapping filter. (Contributed by Jeff Hankins, 26-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐿 = (𝑌filGen𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐶 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ (𝐴 ⊆ 𝑋 ∧ ∃𝑥 ∈ 𝐿 (𝐹 “ 𝑥) ⊆ 𝐴)))
Theorem	fmfg 23460	The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐿 = (𝑌filGen𝐵)    ⇒   ⊢ ((𝑋 ∈ 𝐶 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = ((𝑋 FilMap 𝐹)‘𝐿))
Theorem	elfm3 23461*	An alternate formulation of elementhood in a mapping filter that requires 𝐹 to be onto. (Contributed by Jeff Hankins, 1-Oct-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐿 = (𝑌filGen𝐵)    ⇒   ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌–onto→𝑋) → (𝐴 ∈ ((𝑋 FilMap 𝐹)‘𝐵) ↔ ∃𝑥 ∈ 𝐿 𝐴 = (𝐹 “ 𝑥)))
Theorem	imaelfm 23462	An image of a filter element is in the image filter. (Contributed by Jeff Hankins, 5-Oct-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐿 = (𝑌filGen𝐵)    ⇒   ⊢ (((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑆 ∈ 𝐿) → (𝐹 “ 𝑆) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
Theorem	rnelfmlem 23463*	Lemma for rnelfm 23464. (Contributed by Jeff Hankins, 14-Nov-2009.)
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))
Theorem	rnelfm 23464	A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) → (𝐿 ∈ ran (𝑋 FilMap 𝐹) ↔ ran 𝐹 ∈ 𝐿))
Theorem	fmfnfmlem1 23465*	Lemma for fmfnfm 23469. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
Theorem	fmfnfmlem2 23466*	Lemma for fmfnfm 23469. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
Theorem	fmfnfmlem3 23467*	Lemma for fmfnfm 23469. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
Theorem	fmfnfmlem4 23468*	Lemma for fmfnfm 23469. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
Theorem	fmfnfm 23469*	A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
Theorem	fmufil 23470	An image filter of an ultrafilter is an ultrafilter. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐿 ∈ (UFil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐿) ∈ (UFil‘𝑋))
Theorem	fmid 23471	The filter map applied to the identity. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Mario Carneiro, 27-Aug-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝑋 FilMap ( I ↾ 𝑋))‘𝐹) = 𝐹)
Theorem	fmco 23472	Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)))
Theorem	ufldom 23473	The ultrafilter lemma property is a cardinal invariant, so since it transfers to subsets it also transfers over set dominance. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝑋 ∈ UFL ∧ 𝑌 ≼ 𝑋) → 𝑌 ∈ UFL)
Theorem	flimval 23474*	The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil) → (𝐽 fLim 𝐹) = {𝑥 ∈ 𝑋 ∣ (((nei‘𝐽)‘{𝑥}) ⊆ 𝐹 ∧ 𝐹 ⊆ 𝒫 𝑋)})
Theorem	elflim2 23475	The predicate "is a limit point of a filter." (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ((𝐽 ∈ Top ∧ 𝐹 ∈ ∪ ran Fil ∧ 𝐹 ⊆ 𝒫 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
Theorem	flimtop 23476	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐽 ∈ Top)
Theorem	flimneiss 23477	A filter contains the neighborhood filter as a subfilter. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)
Theorem	flimnei 23478	A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.)
⊢ ((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑁 ∈ 𝐹)
Theorem	flimelbas 23479	A limit point of a filter belongs to its base set. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐴 ∈ 𝑋)
Theorem	flimfil 23480	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → 𝐹 ∈ (Fil‘𝑋))
Theorem	flimtopon 23481	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋)))
Theorem	elflim 23482	The predicate "is a limit point of a filter." (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ 𝐹)))
Theorem	flimss2 23483	A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐺 ⊆ 𝐹) → (𝐽 fLim 𝐺) ⊆ (𝐽 fLim 𝐹))
Theorem	flimss1 23484	A limit point of a filter is a limit point in a coarser topology. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fLim 𝐹) ⊆ (𝐽 fLim 𝐹))
Theorem	neiflim 23485	A point is a limit point of its neighborhood filter. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ (𝐽 fLim ((nei‘𝐽)‘{𝐴})))
Theorem	flimopn 23486*	The condition for being a limit point of a filter still holds if one only considers open neighborhoods. (Contributed by Jeff Hankins, 4-Sep-2009.) (Proof shortened by Mario Carneiro, 9-Apr-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹))))
Theorem	fbflim 23487*	A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐹 = (𝑋filGen𝐵)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝐴 ∈ 𝑥 → ∃𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥))))
Theorem	fbflim2 23488*	A condition for a filter base 𝐵 to converge to a point 𝐴. Use neighborhoods instead of open neighborhoods. Compare fbflim 23487. (Contributed by FL, 4-Jul-2011.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐹 = (𝑋filGen𝐵)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛)))
Theorem	flimclsi 23489	The convergent points of a filter are a subset of the closure of any of the filter sets. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ (𝑆 ∈ 𝐹 → (𝐽 fLim 𝐹) ⊆ ((cls‘𝐽)‘𝑆))
Theorem	hausflimlem 23490	If 𝐴 and 𝐵 are both limits of the same filter, then all neighborhoods of 𝐴 and 𝐵 intersect. (Contributed by Mario Carneiro, 21-Sep-2015.)
⊢ (((𝐴 ∈ (𝐽 fLim 𝐹) ∧ 𝐵 ∈ (𝐽 fLim 𝐹)) ∧ (𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽) ∧ (𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉)) → (𝑈 ∩ 𝑉) ≠ ∅)
Theorem	hausflimi 23491*	One direction of hausflim 23492. A filter in a Hausdorff space has at most one limit. (Contributed by FL, 14-Nov-2010.) (Revised by Mario Carneiro, 21-Sep-2015.)
⊢ (𝐽 ∈ Haus → ∃*𝑥 𝑥 ∈ (𝐽 fLim 𝐹))
Theorem	hausflim 23492*	A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Top ∧ ∀𝑓 ∈ (Fil‘𝑋)∃*𝑥 𝑥 ∈ (𝐽 fLim 𝑓)))
Theorem	flimcf 23493*	Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fLim 𝑓) ⊆ (𝐽 fLim 𝑓)))
Theorem	flimrest 23494	The set of limit points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐽 ↾t 𝑌) fLim (𝐹 ↾t 𝑌)) = ((𝐽 fLim 𝐹) ∩ 𝑌))
Theorem	flimclslem 23495	Lemma for flimcls 23496. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹)))
Theorem	flimcls 23496*	Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓 ∈ (Fil‘𝑋)(𝑆 ∈ 𝑓 ∧ 𝐴 ∈ (𝐽 fLim 𝑓))))
Theorem	flimsncls 23497	If 𝐴 is a limit point of the filter 𝐹, then all the points which specialize 𝐴 (in the specialization preorder) are also limit points. Thus, the set of limit points is a union of closed sets (although this is only nontrivial for non-T1 spaces). (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → ((cls‘𝐽)‘{𝐴}) ⊆ (𝐽 fLim 𝐹))
Theorem	hauspwpwf1 23498*	Lemma for hauspwpwdom 23499. Points in the closure of a set in a Hausdorff space are characterized by the open neighborhoods they extend into the generating set. (Contributed by Mario Carneiro, 28-Jul-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐹 = (𝑥 ∈ ((cls‘𝐽)‘𝐴) ↦ {𝑎 ∣ ∃𝑗 ∈ 𝐽 (𝑥 ∈ 𝑗 ∧ 𝑎 = (𝑗 ∩ 𝐴))})    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋) → 𝐹:((cls‘𝐽)‘𝐴)–1-1→𝒫 𝒫 𝐴)
Theorem	hauspwpwdom 23499	If 𝑋 is a Hausdorff space, then the cardinality of the closure of a set 𝐴 is bounded by the double powerset of 𝐴. In particular, a Hausdorff space with a dense subset 𝐴 has cardinality at most 𝒫 𝒫 𝐴, and a separable Hausdorff space has cardinality at most 𝒫 𝒫 ℕ. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 28-Jul-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘𝐴) ≼ 𝒫 𝒫 𝐴)
Theorem	flffval 23500*	Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌)) → (𝐽 fLimf 𝐿) = (𝑓 ∈ (𝑋 ↑m 𝑌) ↦ (𝐽 fLim ((𝑋 FilMap 𝑓)‘𝐿))))