P. 230 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22901-23000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opnfbas 22901*	The collection of open supersets of a nonempty set in a topology is a neighborhoods of the set, one of the motivations for the filter concept. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋))
Theorem	trfbas2 22902	Conditions for the trace of a filter base 𝐹 to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐹 ↾t 𝐴) ∈ (fBas‘𝐴) ↔ ¬ ∅ ∈ (𝐹 ↾t 𝐴)))
Theorem	trfbas 22903*	Conditions for the trace of a filter base 𝐹 to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐹 ↾t 𝐴) ∈ (fBas‘𝐴) ↔ ∀𝑣 ∈ 𝐹 (𝑣 ∩ 𝐴) ≠ ∅))
12.2.2  Filters
Syntax	cfil 22904	Extend class notation with the set of filters on a set.
class Fil
Definition	df-fil 22905*	The set of filters on a set. Definition 1 (axioms FI, FIIa, FIIb, FIII) of [BourbakiTop1] p. I.36. Filters are used to define the concept of limit in the general case. They are a generalization of the idea of neighborhoods. Suppose you are in ℝ. With neighborhoods you can express the idea of a variable that tends to a specific number but you can't express the idea of a variable that tends to infinity. Filters relax the "axioms" of neighborhoods and then succeed in expressing the idea of something that tends to infinity. Filters were invented by Cartan in 1937 and made famous by Bourbaki in his treatise. A notion similar to the notion of filter is the concept of net invented by Moore and Smith in 1922. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ Fil = (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)})
Theorem	isfil 22906*	The predicate "is a filter." (Contributed by FL, 20-Jul-2007.) (Revised by Mario Carneiro, 28-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)))
Theorem	filfbas 22907	A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋))
Theorem	0nelfil 22908	The empty set doesn't belong to a filter. (Contributed by FL, 20-Jul-2007.) (Revised by Mario Carneiro, 28-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐹)
Theorem	fileln0 22909	An element of a filter is nonempty. (Contributed by FL, 24-May-2011.) (Revised by Mario Carneiro, 28-Jul-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ≠ ∅)
Theorem	filsspw 22910	A filter is a subset of the power set of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
Theorem	filelss 22911	An element of a filter is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ 𝑋)
Theorem	filss 22912	A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ 𝐹)
Theorem	filin 22913	A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ∩ 𝐵) ∈ 𝐹)
Theorem	filtop 22914	The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹)
Theorem	isfil2 22915*	Derive the standard axioms of a filter. (Contributed by Mario Carneiro, 27-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹))
Theorem	isfildlem 22916*	Lemma for isfild 22917. (Contributed by Mario Carneiro, 1-Dec-2013.)
⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓)))
Theorem	isfild 22917*	Sufficient condition for a set of the form {𝑥 ∈ 𝒫 𝐴 ∣ 𝜑} to be a filter. (Contributed by Mario Carneiro, 1-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) (Revised by AV, 10-Apr-2024.)
⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → [𝐴 / 𝑥]𝜓)    &   ⊢ (𝜑 → ¬ [∅ / 𝑥]𝜓)    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦) → ([𝑧 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜓))    &   ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴) → (([𝑦 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜓) → [(𝑦 ∩ 𝑧) / 𝑥]𝜓))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (Fil‘𝐴))
Theorem	filfi 22918	A filter is closed under taking intersections. (Contributed by Mario Carneiro, 27-Nov-2013.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹)
Theorem	filinn0 22919	The intersection of two elements of a filter can't be empty. (Contributed by FL, 16-Sep-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ∩ 𝐵) ≠ ∅)
Theorem	filintn0 22920	A filter has the finite intersection property. Remark below Definition 1 of [BourbakiTop1] p. I.36. (Contributed by FL, 20-Sep-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴 ⊆ 𝐹 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ≠ ∅)
Theorem	filn0 22921	The empty set is not a filter. Remark below Definition 1 of [BourbakiTop1] p. I.36. (Contributed by FL, 30-Oct-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅)
Theorem	infil 22922	The intersection of two filters is a filter. Use fiint 9021 to extend this property to the intersection of a finite set of filters. Paragraph 3 of [BourbakiTop1] p. I.36. (Contributed by FL, 17-Sep-2007.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋)) → (𝐹 ∩ 𝐺) ∈ (Fil‘𝑋))
Theorem	snfil 22923	A singleton is a filter. Example 1 of [BourbakiTop1] p. I.36. (Contributed by FL, 16-Sep-2007.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → {𝐴} ∈ (Fil‘𝐴))
Theorem	fbasweak 22924	A filter base on any set is also a filter base on any larger set. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐹 ∈ (fBas‘𝑌))
Theorem	snfbas 22925	Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ 𝑉) → {𝐴} ∈ (fBas‘𝐵))
Theorem	fsubbas 22926	A condition for a set to generate a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝑋 ∈ 𝑉 → ((fi‘𝐴) ∈ (fBas‘𝑋) ↔ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ (fi‘𝐴))))
Theorem	fbasfip 22927	A filter base has the finite intersection property. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈ (fi‘𝐹))
Theorem	fbunfip 22928*	A helpful lemma for showing that certain sets generate filters. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐺 ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ 𝐺)) ↔ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐺 (𝑥 ∩ 𝑦) ≠ ∅))
Theorem	fgval 22929*	The filter generating class gives a filter for every filter base. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝐹 ∩ 𝒫 𝑥) ≠ ∅})
Theorem	elfg 22930*	A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝐴 ∈ (𝑋filGen𝐹) ↔ (𝐴 ⊆ 𝑋 ∧ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴)))
Theorem	ssfg 22931	A filter base is a subset of its generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
Theorem	fgss 22932	A bigger base generates a bigger filter. (Contributed by NM, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐺 ∈ (fBas‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝑋filGen𝐹) ⊆ (𝑋filGen𝐺))
Theorem	fgss2 22933*	A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐺 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐹) ⊆ (𝑋filGen𝐺) ↔ ∀𝑥 ∈ 𝐹 ∃𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥))
Theorem	fgfil 22934	A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹)
Theorem	elfilss 22935*	An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴))
Theorem	filfinnfr 22936	No filter containing a finite element is free. (Contributed by Jeff Hankins, 5-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝑆 ∈ Fin) → ∩ 𝐹 ≠ ∅)
Theorem	fgcl 22937	A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
Theorem	fgabs 22938	Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
Theorem	neifil 22939	The neighborhoods of a nonempty set is a filter. Example 2 of [BourbakiTop1] p. I.36. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((nei‘𝐽)‘𝑆) ∈ (Fil‘𝑋))
Theorem	filunibas 22940	Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 = 𝑋)
Theorem	filunirn 22941	Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ (Fil‘∪ 𝐹))
Theorem	filconn 22942	A filter gives rise to a connected topology. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈ Conn)
Theorem	fbasrn 22943*	Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥))    ⇒   ⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ∈ (fBas‘𝑌))
Theorem	filuni 22944*	The union of a nonempty set of filters with a common base and closed under pairwise union is a filter. (Contributed by Mario Carneiro, 28-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐹 (𝑓 ∪ 𝑔) ∈ 𝐹) → ∪ 𝐹 ∈ (Fil‘𝑋))
Theorem	trfil1 22945	Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by FL, 2-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 = ∪ (𝐿 ↾t 𝐴))
Theorem	trfil2 22946*	Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by FL, 2-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅))
Theorem	trfil3 22947	Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ (𝑌 ∖ 𝐴) ∈ 𝐿))
Theorem	trfilss 22948	If 𝐴 is a member of the filter, then the filter truncated to 𝐴 is a subset of the original filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝐹 ↾t 𝐴) ⊆ 𝐹)
Theorem	fgtr 22949	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 22950	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 22949 for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐹 ∈ (Fil‘𝐴) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉) → ((𝑋filGen𝐹) ↾t 𝐴) = 𝐹)
Theorem	trnei 22951	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 22946 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 22952*	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 22953*	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 22954*	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 22955	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 22956	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 22957	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 22958	Extend class notation with the ultrafilters-on-a-set function.
class UFil
Syntax	cufl 22959	Extend class notation with the ultrafilter lemma.
class UFL
Definition	df-ufil 22960*	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 22961*	Define the class of base sets for which the ultrafilter lemma filssufil 22971 holds. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ UFL = {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔}
Theorem	isufil 22962*	The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)))
Theorem	ufilfil 22963	An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋))
Theorem	ufilss 22964	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 22965	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 22966	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 22967*	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 22968	An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Mario Carneiro, 2-Aug-2015.)
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((𝐴 ∈ 𝐹 ∨ 𝐵 ∈ 𝐹) ↔ (𝐴 ∪ 𝐵) ∈ 𝐹))
Theorem	trufil 22969	Conditions for the trace of an ultrafilter 𝐿 to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((𝐿 ∈ (UFil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (UFil‘𝐴) ↔ 𝐴 ∈ 𝐿))
Theorem	filssufilg 22970*	A filter is contained in some ultrafilter. This version of filssufil 22971 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 22971*	A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 10157.) (Contributed by Jeff Hankins, 2-Dec-2009.) (Revised by Stefan O'Rear, 29-Jul-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
Theorem	isufl 22972*	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 22973*	Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝑋 ∈ UFL ∧ 𝐹 ∈ (Fil‘𝑋)) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓)
Theorem	numufl 22974	Consequence of filssufilg 22970: a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL)
Theorem	fiufl 22975	A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝑋 ∈ Fin → 𝑋 ∈ UFL)
Theorem	acufl 22976	The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (CHOICE → UFL = V)
Theorem	ssufl 22977	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 22978*	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 22979*	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 22980*	Lemma for fixufil 22981 and uffixfr 22982. (Contributed by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → ({{𝐴}} ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} = (𝑋filGen{{𝐴}})))
Theorem	fixufil 22981*	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 22982*	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 22983*	A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 ≠ ∅ ↔ ∃𝑥 ∈ 𝑋 𝐹 = {𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦}))
Theorem	uffixsn 22984	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 22985	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 22986*	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 22987*	An ultrafilter is free iff it contains the Fréchet filter cfinfil 22952 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 = ∅ ↔ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹))
Theorem	ufinffr 22988*	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 22989*	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 22990	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 22991	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 22992	Extend class definition to include the neighborhood filter mapping function.
class FilMap
Syntax	cflim 22993	Extend class notation with a function returning the limit of a filter.
class fLim
Syntax	cflf 22994	Extend class definition to include the function for filter-based function limits.
class fLimf
Syntax	cfcls 22995	Extend class definition to include the cluster point function on filters.
class fClus
Syntax	cfcf 22996	Extend class definition to include the function for cluster points of a function.
class fClusf
Definition	df-fm 22997*	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 22998*	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 22999*	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 23000*	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‘𝑗)‘𝑥), ∅))