P. 223 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22201-22300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	flimcls 22201*	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 22202	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 22203*	Lemma for hauspwpwdom 22204. 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 22204	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 22205*	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 22206	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 22207*	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 22208*	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 22209*	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 22210	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 22211*	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 22212*	Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (topGen‘𝐵)    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐵 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑜))))
Theorem	hausflf 22213*	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 22214	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 22215	Forward direction of cnpflf 22217. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐴 ∈ (𝐽 fLim 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹))
Theorem	cnpflf2 22216	𝐹 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 22217*	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 22218*	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 22219*	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 22220	A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹)))
Theorem	lmflf 22221	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 22222*	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 22223*	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 22224*	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 22225*	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 22226	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 22227	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 22228	Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐴 ∈ (𝐽 fClus 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋)))
Theorem	isfcls2 22229*	A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∀𝑠 ∈ 𝐹 𝐴 ∈ ((cls‘𝐽)‘𝑠)))
Theorem	fclsopn 22230*	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 22231	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 22232	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 22233	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 22234	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 22235*	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 22236*	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 22237*	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 22238	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 22239	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 22240	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 22241*	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 22242	A limit point is a cluster point. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝐽 fLim 𝐹) ⊆ (𝐽 fClus 𝐹)
Theorem	fclsfnflim 22243*	A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fClus 𝐹) ↔ ∃𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 ∧ 𝐴 ∈ (𝐽 fLim 𝑔))))
Theorem	flimfnfcls 22244*	A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 22243, this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ ∀𝑔 ∈ (Fil‘𝑋)(𝐹 ⊆ 𝑔 → 𝐴 ∈ (𝐽 fClus 𝑔))))
Theorem	fclscmpi 22245	Forward direction of fclscmp 22246. Every filter clusters in a compact space. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝐽 fClus 𝐹) ≠ ∅)
Theorem	fclscmp 22246*	A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Comp ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝐽 fClus 𝑓) ≠ ∅))
Theorem	uffclsflim 22247	The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 fClus 𝐹) = (𝐽 fLim 𝐹))
Theorem	ufilcmp 22248*	A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009.) (Proof shortened by Mario Carneiro, 12-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝑋 ∈ UFL ∧ 𝐽 ∈ (TopOn‘𝑋)) → (𝐽 ∈ Comp ↔ ∀𝑓 ∈ (UFil‘𝑋)(𝐽 fLim 𝑓) ≠ ∅))
Theorem	fcfval 22249	The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fClusf 𝐿)‘𝐹) = (𝐽 fClus ((𝑋 FilMap 𝐹)‘𝐿)))
Theorem	isfcf 22250*	The property of being a cluster point of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∀𝑠 ∈ 𝐿 (𝑜 ∩ (𝐹 “ 𝑠)) ≠ ∅))))
Theorem	fcfnei 22251*	The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∀𝑠 ∈ 𝐿 (𝑛 ∩ (𝐹 “ 𝑠)) ≠ ∅)))
Theorem	fcfelbas 22252	A cluster point of a function is in the base set of the topology. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹)) → 𝐴 ∈ 𝑋)
Theorem	fcfneii 22253	A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fClusf 𝐿)‘𝐹) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝐴}) ∧ 𝑆 ∈ 𝐿)) → (𝑁 ∩ (𝐹 “ 𝑆)) ≠ ∅)
Theorem	flfssfcf 22254	A limit point of a function is a cluster point of the function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fLimf 𝐿)‘𝐹) ⊆ ((𝐽 fClusf 𝐿)‘𝐹))
Theorem	uffcfflf 22255	If the domain filter is an ultrafilter, the cluster points of the function are the limit points. (Contributed by Jeff Hankins, 12-Dec-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (UFil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fClusf 𝐿)‘𝐹) = ((𝐽 fLimf 𝐿)‘𝐹))
Theorem	cnpfcfi 22256	Lemma for cnpfcf 22257. If a function is continuous at a point, it respects clustering there. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝐿)‘𝐹))
Theorem	cnpfcf 22257*	A function 𝐹 is continuous at point 𝐴 iff 𝐹 respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))
Theorem	cnfcf 22258*	Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fClus 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))
Theorem	flfcntr 22259	A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (𝐹‘𝑋) ∈ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))
Theorem	alexsublem 22260*	Lemma for alexsub 22261. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝜑 → 𝑋 ∈ UFL)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐵)    &   ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵)))    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)    &   ⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋))    &   ⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅)    ⇒   ⊢ ¬ 𝜑
Theorem	alexsub 22261*	The Alexander Subbase Theorem: If 𝐵 is a subbase for the topology 𝐽, and any cover taken from 𝐵 has a finite subcover, then the generated topology is compact. This proof uses the ultrafilter lemma; see alexsubALT 22267 for a proof using Zorn's lemma. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 26-Aug-2015.)
⊢ (𝜑 → 𝑋 ∈ UFL)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐵)    &   ⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵)))    &   ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)    ⇒   ⊢ (𝜑 → 𝐽 ∈ Comp)
Theorem	alexsubb 22262*	Biconditional form of the Alexander Subbase Theorem alexsub 22261. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((𝑋 ∈ UFL ∧ 𝑋 = ∪ 𝐵) → ((topGen‘(fi‘𝐵)) ∈ Comp ↔ ∀𝑥 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑥 → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦)))
Theorem	alexsubALTlem1 22263*	Lemma for alexsubALT 22267. A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
Theorem	alexsubALTlem2 22264*	Lemma for alexsubALT 22267. Every subset of a base which has no finite subcover is a subset of a maximal such collection. (Contributed by Jeff Hankins, 27-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ ∀𝑏 ∈ (𝒫 𝑎 ∩ Fin) ¬ 𝑋 = ∪ 𝑏) → ∃𝑢 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅})∀𝑣 ∈ ({𝑧 ∈ 𝒫 (fi‘𝑥) ∣ (𝑎 ⊆ 𝑧 ∧ ∀𝑏 ∈ (𝒫 𝑧 ∩ Fin) ¬ 𝑋 = ∪ 𝑏)} ∪ {∅}) ¬ 𝑢 ⊊ 𝑣)
Theorem	alexsubALTlem3 22265*	Lemma for alexsubALT 22267. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) ∧ 𝑎 ∈ 𝒫 (fi‘𝑥)) ∧ (𝑢 ∈ 𝒫 (fi‘𝑥) ∧ (𝑎 ⊆ 𝑢 ∧ ∀𝑏 ∈ (𝒫 𝑢 ∩ Fin) ¬ 𝑋 = ∪ 𝑏))) ∧ 𝑤 ∈ 𝑢) ∧ ((𝑡 ∈ (𝒫 𝑥 ∩ Fin) ∧ 𝑤 = ∩ 𝑡) ∧ (𝑦 ∈ 𝑤 ∧ ¬ 𝑦 ∈ ∪ (𝑥 ∩ 𝑢)))) → ∃𝑠 ∈ 𝑡 ∀𝑛 ∈ (𝒫 (𝑢 ∪ {𝑠}) ∩ Fin) ¬ 𝑋 = ∪ 𝑛)
Theorem	alexsubALTlem4 22266*	Lemma for alexsubALT 22267. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏)))
Theorem	alexsubALT 22267*	The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))
Theorem	ptcmplem1 22268*	Lemma for ptcmp 22274. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Comp)    &   ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))    ⇒   ⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))))
Theorem	ptcmplem2 22269*	Lemma for ptcmp 22274. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Comp)    &   ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))    &   ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)    ⇒   ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card)
Theorem	ptcmplem3 22270*	Lemma for ptcmp 22274. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Comp)    &   ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))    &   ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)    &   ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}    ⇒   ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
Theorem	ptcmplem4 22271*	Lemma for ptcmp 22274. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Comp)    &   ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))    &   ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆)    &   ⊢ (𝜑 → 𝑋 = ∪ 𝑈)    &   ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)    &   ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}    ⇒   ⊢ ¬ 𝜑
Theorem	ptcmplem5 22272*	Lemma for ptcmp 22274. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))    &   ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Comp)    &   ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))    ⇒   ⊢ (𝜑 → (∏t‘𝐹) ∈ Comp)
Theorem	ptcmpg 22273	Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if 𝒫 𝒫 𝑋 is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp 22274). (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ 𝐽 = (∏t‘𝐹)    &   ⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Comp ∧ 𝑋 ∈ (UFL ∩ dom card)) → 𝐽 ∈ Comp)
Theorem	ptcmp 22274	Tychonoff's theorem: The product of compact spaces is compact. The proof uses the Axiom of Choice. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp)
12.2.5  Extension by continuity
Syntax	ccnext 22275	Extend class notation with the continuous extension operation.
class CnExt
Definition	df-cnext 22276*	Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017.)
⊢ CnExt = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑓 ∈ (∪ 𝑘 ↑pm ∪ 𝑗) ↦ ∪ 𝑥 ∈ ((cls‘𝑗)‘dom 𝑓)({𝑥} × ((𝑘 fLimf (((nei‘𝑗)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))
Theorem	cnextval 22277*	The function applying continuous extension to a given function 𝑓. (Contributed by Thierry Arnoux, 1-Dec-2017.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽CnExt𝐾) = (𝑓 ∈ (∪ 𝐾 ↑pm ∪ 𝐽) ↦ ∪ 𝑥 ∈ ((cls‘𝐽)‘dom 𝑓)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t dom 𝑓))‘𝑓))))
Theorem	cnextfval 22278*	The continuous extension of a given function 𝐹. (Contributed by Thierry Arnoux, 1-Dec-2017.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝑋)) → ((𝐽CnExt𝐾)‘𝐹) = ∪ 𝑥 ∈ ((cls‘𝐽)‘𝐴)({𝑥} × ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹)))
Theorem	cnextrel 22279	In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Rel ((𝐽CnExt𝐾)‘𝐹))
Theorem	cnextfun 22280	If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Haus) ∧ (𝐹:𝐴⟶𝐵 ∧ 𝐴 ⊆ 𝐶)) → Fun ((𝐽CnExt𝐾)‘𝐹))
Theorem	cnextfvval 22281*	The value of the continuous extension of a given function 𝐹 at a point 𝑋. (Contributed by Thierry Arnoux, 21-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = ∪ ((𝐾 fLimf (((nei‘𝐽)‘{𝑋}) ↾t 𝐴))‘𝐹))
Theorem	cnextf 22282*	Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹):𝐶⟶𝐵)
Theorem	cnextcn 22283*	Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology 𝐽 on 𝐶, a subset 𝐴 dense in 𝐶, this states a condition for 𝐹 from 𝐴 to a regular space 𝐾 to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ Reg)    ⇒   ⊢ (𝜑 → ((𝐽CnExt𝐾)‘𝐹) ∈ (𝐽 Cn 𝐾))
Theorem	cnextfres1 22284*	𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 17-Jan-2018.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ((𝐾 fLimf (((nei‘𝐽)‘{𝑥}) ↾t 𝐴))‘𝐹) ≠ ∅)    &   ⊢ (𝜑 → 𝐾 ∈ Reg)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))    ⇒   ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹) ↾ 𝐴) = 𝐹)
Theorem	cnextfres 22285	𝐹 and its extension by continuity agree on the domain of 𝐹. (Contributed by Thierry Arnoux, 29-Aug-2020.)
⊢ 𝐶 = ∪ 𝐽    &   ⊢ 𝐵 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ Top)    &   ⊢ (𝜑 → 𝐾 ∈ Haus)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐶)    &   ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ↾t 𝐴) Cn 𝐾))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → (((𝐽CnExt𝐾)‘𝐹)‘𝑋) = (𝐹‘𝑋))
12.2.6  Topological groups
Syntax	ctmd 22286	Extend class notation with the class of all topological monoids.
class TopMnd
Syntax	ctgp 22287	Extend class notation with the class of all topological groups.
class TopGrp
Definition	df-tmd 22288*	Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ TopMnd = {𝑓 ∈ (Mnd ∩ TopSp) ∣ [(TopOpen‘𝑓) / 𝑗](+𝑓‘𝑓) ∈ ((𝑗 ×t 𝑗) Cn 𝑗)}
Definition	df-tgp 22289*	Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010.)
⊢ TopGrp = {𝑓 ∈ (Grp ∩ TopMnd) ∣ [(TopOpen‘𝑓) / 𝑗](invg‘𝑓) ∈ (𝑗 Cn 𝑗)}
Theorem	istmd 22290	The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐹 = (+𝑓‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopMnd ↔ (𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)))
Theorem	tmdmnd 22291	A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ Mnd)
Theorem	tmdtps 22292	A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp)
Theorem	istgp 22293	The predicate "is a topological group". Definition 1 of [BourbakiTop1] p. III.1. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ TopMnd ∧ 𝐼 ∈ (𝐽 Cn 𝐽)))
Theorem	tgpgrp 22294	A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ Grp)
Theorem	tgptmd 22295	A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd)
Theorem	tgptps 22296	A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐺 ∈ TopGrp → 𝐺 ∈ TopSp)
Theorem	tmdtopon 22297	The topology of a topological monoid. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopMnd → 𝐽 ∈ (TopOn‘𝑋))
Theorem	tgptopon 22298	The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝐽 ∈ (TopOn‘𝑋))
Theorem	tmdcn 22299	In a topological monoid, the operation 𝐹 representing the functionalization of the operator slot +g is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopMnd → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
Theorem	tgpcn 22300	In a topological group, the operation 𝐹 representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 = (TopOpen‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ TopGrp → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽))