P. 222 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22101-22200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	uffinfix 22101*	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 22102*	An ultrafilter is free iff it contains the Fréchet filter cfinfil 22067 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 = ∅ ↔ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹))
Theorem	ufinffr 22103*	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 22104*	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 22105	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 22106	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 22107	Extend class definition to include the neighborhood filter mapping function.
class FilMap
Syntax	cflim 22108	Extend class notation with a function returning the limit of a filter.
class fLim
Syntax	cflf 22109	Extend class definition to include the function for filter-based function limits.
class fLimf
Syntax	cfcls 22110	Extend class definition to include the cluster point function on filters.
class fClus
Syntax	cfcf 22111	Extend class definition to include the function for cluster points of a function.
class fClusf
Definition	df-fm 22112*	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 22113*	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 22114*	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 ↦ (𝑓 ∈ (∪ 𝑥 ↑𝑚 ∪ 𝑦) ↦ (𝑥 fLim ((∪ 𝑥 FilMap 𝑓)‘𝑦))))
Definition	df-fcls 22115*	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 22116*	Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.)
⊢ fClusf = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑𝑚 ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓))))
Theorem	fmval 22117*	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 22118	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 22119	Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋))
Theorem	fmss 22120	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 22121*	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 22122*	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 22123	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 22124*	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 22125	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 22126*	Lemma for rnelfm 22127. (Contributed by Jeff Hankins, 14-Nov-2009.)
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))
Theorem	rnelfm 22127	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 22128*	Lemma for fmfnfm 22132. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
Theorem	fmfnfmlem2 22129*	Lemma for fmfnfm 22132. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))))
Theorem	fmfnfmlem3 22130*	Lemma for fmfnfm 22132. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))
Theorem	fmfnfmlem4 22131*	Lemma for fmfnfm 22132. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑌⟶𝑋)    &   ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)    ⇒   ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
Theorem	fmfnfm 22132*	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 22133	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 22134	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 22135	Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵)))
Theorem	ufldom 22136	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 22137*	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 22138	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 22139	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 22140	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 22141	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 22142	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 22143	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 22144	Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋)))
Theorem	elflim 22145	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 22146	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 22147	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 22148	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 22149*	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 22150*	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 22151*	A condition for a filter base 𝐵 to converge to a point 𝐴. Use neighborhoods instead of open neighborhoods. Compare fbflim 22150. (Contributed by FL, 4-Jul-2011.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐹 = (𝑋filGen𝐵)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛)))
Theorem	flimclsi 22152	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 22153	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 22154*	One direction of hausflim 22155. 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 22155*	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 22156*	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 22157	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 22158	Lemma for flimcls 22159. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆})))    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹)))
Theorem	flimcls 22159*	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 22160	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 22161*	Lemma for hauspwpwdom 22162. 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 22162	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 22163*	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 𝐿) = (𝑓 ∈ (𝑋 ↑𝑚 𝑌) ↦ (𝐽 fLim ((𝑋 FilMap 𝑓)‘𝐿))))
Theorem	flfval 22164	Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fLimf 𝐿)‘𝐹) = (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿)))
Theorem	flfnei 22165*	The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛)))
Theorem	flfneii 22166*	A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴})) → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑁)
Theorem	isflf 22167*	The property of being a limit point of a function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑜))))
Theorem	flfelbas 22168	A limit point of a function is in the topological space. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹)) → 𝐴 ∈ 𝑋)
Theorem	flffbas 22169*	Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ 𝐿 = (𝑌filGen𝐵)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))))
Theorem	flftg 22170*	Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (topGen‘𝐵)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐵 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑜))))
Theorem	hausflf 22171*	If a function has its values in a Hausdorff space, then it has at most one limit value. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ∃*𝑥 𝑥 ∈ ((𝐽 fLimf 𝐿)‘𝐹))
Theorem	hausflf2 22172	If a convergent function has its values in a Hausdorff space, then it has a unique limit. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Haus ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ ((𝐽 fLimf 𝐿)‘𝐹) ≠ ∅) → ((𝐽 fLimf 𝐿)‘𝐹) ≈ 1o)
Theorem	cnpflfi 22173	Forward direction of cnpflf 22175. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐴 ∈ (𝐽 fLim 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹))
Theorem	cnpflf2 22174	𝐹 is continuous at point 𝐴 iff a limit of 𝐹 when 𝑥 tends to 𝐴 is (𝐹‘𝐴). Proposition 9 of [BourbakiTop1] p. TG I.50. (Contributed by FL, 29-May-2011.) (Revised by Mario Carneiro, 9-Apr-2015.)
⊢ 𝐿 = ((nei‘𝐽)‘{𝐴})    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹))))
Theorem	cnpflf 22175*	Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))))
Theorem	cnflf 22176*	A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
Theorem	cnflf2 22177*	A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 “ (𝐽 fLim 𝑓)) ⊆ ((𝐾 fLimf 𝑓)‘𝐹))))
Theorem	flfcnp 22178	A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹)))
Theorem	lmflf 22179	The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐿 = (𝑍filGen(ℤ≥ “ 𝑍))    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹)))
Theorem	txflf 22180*	Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍))    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ (𝜑 → 𝐺:𝑍⟶𝑌)    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ ⟨(𝐹‘𝑛), (𝐺‘𝑛)⟩)    ⇒   ⊢ (𝜑 → (⟨𝑅, 𝑆⟩ ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺))))
Theorem	flfcnp2 22181*	The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐴)))    &   ⊢ (𝜑 → 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐵)))    &   ⊢ (𝜑 → 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘⟨𝑅, 𝑆⟩))    ⇒   ⊢ (𝜑 → (𝑅𝑂𝑆) ∈ ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵))))
Theorem	fclsval 22182*	The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑌)) → (𝐽 fClus 𝐹) = if(𝑋 = 𝑌, ∩ 𝑡 ∈ 𝐹 ((cls‘𝐽)‘𝑡), ∅))
Theorem	isfcls 22183*	A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))
Theorem	fclsfil 22184	Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐹 ∈ (Fil‘𝑋))
Theorem	fclstop 22185	Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐽 ∈ Top)
Theorem	fclstopon 22186	Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋)))
Theorem	isfcls2 22187*	A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))
Theorem	fclsopn 22188*	Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐹 (𝑜 ∩ 𝑠) ≠ ∅))))
Theorem	fclsopni 22189	An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ (𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈 ∧ 𝑆 ∈ 𝐹)) → (𝑈 ∩ 𝑆) ≠ ∅)
Theorem	fclselbas 22190	A cluster point is in the base set. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → 𝐴 ∈ 𝑋)
Theorem	fclsneii 22191	A neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐴 ∈ (𝐽 fClus 𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐹) → (𝑁 ∩ 𝑆) ≠ ∅)
Theorem	fclssscls 22192	The set of cluster points is a subset of the closure of any filter element. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝑆 ∈ 𝐹 → (𝐽 fClus 𝐹) ⊆ ((cls‘𝐽)‘𝑆))
Theorem	fclsnei 22193*	Cluster points in terms of neighborhoods. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠 ∈ 𝐹 (𝑛 ∩ 𝑠) ≠ ∅)))
Theorem	supnfcls 22194*	The filter of supersets of 𝑋 ∖ 𝑈 does not cluster at any point of the open set 𝑈. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈) → ¬ 𝐴 ∈ (𝐽 fClus {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑈) ⊆ 𝑥}))
Theorem	fclsbas 22195*	Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ 𝐹 = (𝑋filGen𝐵)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐵 (𝑜 ∩ 𝑠) ≠ ∅))))
Theorem	fclsss1 22196	A finer topology has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐽 ⊆ 𝐾) → (𝐾 fClus 𝐹) ⊆ (𝐽 fClus 𝐹))
Theorem	fclsss2 22197	A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝐽 fClus 𝐺) ⊆ (𝐽 fClus 𝐹))
Theorem	fclsrest 22198	The set of cluster points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → ((𝐽 ↾t 𝑌) fClus (𝐹 ↾t 𝑌)) = ((𝐽 fClus 𝐹) ∩ 𝑌))
Theorem	fclscf 22199*	Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑋)) → (𝐽 ⊆ 𝐾 ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐾 fClus 𝑓) ⊆ (𝐽 fClus 𝑓)))
Theorem	flimfcls 22200	A limit point is a cluster point. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝐽 fLim 𝐹) ⊆ (𝐽 fClus 𝐹)