P. 234 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23301-23400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	perfcls 23301	A subset of a perfect space is perfect iff its closure is perfect (and the closure is an actual perfect set, since it is both closed and perfect in the subspace topology). (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ (𝐽 ↾t ((cls‘𝐽)‘𝑆)) ∈ Perf))
Theorem	restt0 23302	A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Kol2 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Kol2)
Theorem	restt1 23303	A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Fre)
Theorem	resthaus 23304	A subspace of a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Haus ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Haus)
Theorem	t1sep2 23305*	Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → 𝐴 = 𝐵))
Theorem	t1sep 23306*	Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜))
Theorem	sncld 23307	A singleton is closed in a Hausdorff space. (Contributed by NM, 5-Mar-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝑃 ∈ 𝑋) → {𝑃} ∈ (Clsd‘𝐽))
Theorem	sshauslem 23308	Lemma for sshaus 23311 and similar theorems. If the topological property 𝐴 is preserved under injective preimages, then a topology finer than one with property 𝐴 also has property 𝐴. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top)    &   ⊢ ((𝐽 ∈ 𝐴 ∧ ( I ↾ 𝑋):𝑋–1-1→𝑋 ∧ ( I ↾ 𝑋) ∈ (𝐾 Cn 𝐽)) → 𝐾 ∈ 𝐴)    ⇒   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ 𝐴)
Theorem	sst0 23309	A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Kol2 ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Kol2)
Theorem	sst1 23310	A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Fre)
Theorem	sshaus 23311	A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Haus)
Theorem	regsep2 23312*	In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Reg ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐴 ∈ 𝑋 ∧ ¬ 𝐴 ∈ 𝐶)) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ 𝐴 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))
Theorem	isreg2 23313*	A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Reg ↔ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑥 ∈ 𝑋 (¬ 𝑥 ∈ 𝑐 → ∃𝑜 ∈ 𝐽 ∃𝑝 ∈ 𝐽 (𝑐 ⊆ 𝑜 ∧ 𝑥 ∈ 𝑝 ∧ (𝑜 ∩ 𝑝) = ∅))))
Theorem	dnsconst 23314	If a continuous mapping to a T1 space is constant on a dense subset, it is constant on the entire space. Note that ((cls‘𝐽)‘𝐴) = 𝑋 means "𝐴 is dense in 𝑋 " and 𝐴 ⊆ (◡𝐹 “ {𝑃}) means "𝐹 is constant on 𝐴 " (see funconstss 7045). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐾 ∈ Fre ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ (◡𝐹 “ {𝑃}) ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐹:𝑋⟶{𝑃})
Theorem	ordtt1 23315	The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ Fre)
Theorem	lmmo 23316	A sequence in a Hausdorff space converges to at most one limit. Part of Lemma 1.4-2(a) of [Kreyszig] p. 26. (Contributed by NM, 31-Jan-2008.) (Proof shortened by Mario Carneiro, 1-May-2014.)
⊢ (𝜑 → 𝐽 ∈ Haus)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐴)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐵)    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	lmfun 23317	The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ (𝐽 ∈ Haus → Fun (⇝𝑡‘𝐽))
Theorem	dishaus 23318	A discrete topology is Hausdorff. Morris, Topology without tears, p.72, ex. 13. (Contributed by FL, 24-Jun-2007.) (Proof shortened by Mario Carneiro, 8-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Haus)
Theorem	ordthauslem 23319*	Lemma for ordthaus 23320. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → (𝐴 ≠ 𝐵 → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))))
Theorem	ordthaus 23320	The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → (ordTop‘𝑅) ∈ Haus)
Theorem	xrhaus 23321	The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ (ordTop‘ ≤ ) ∈ Haus
12.1.11  Compactness
Syntax	ccmp 23322	Extend class notation with the class of all compact spaces.
class Comp
Definition	df-cmp 23323*	Definition of a compact topology. A topology is compact iff any open covering of its underlying set contains a finite subcovering (Heine-Borel property). Definition C''' of [BourbakiTop1] p. I.59. Note: Bourbaki uses the term "quasi-compact" (saving "compact" for "compact Hausdorff"), but it is not the modern usage (which we follow). (Contributed by FL, 22-Dec-2008.)
⊢ Comp = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥(∪ 𝑥 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)∪ 𝑥 = ∪ 𝑧)}
Theorem	iscmp 23324*	The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
Theorem	cmpcov 23325*	An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆) → ∃𝑠 ∈ (𝒫 𝑆 ∩ Fin)𝑋 = ∪ 𝑠)
Theorem	cmpcov2 23326*	Rewrite cmpcov 23325 for the cover {𝑦 ∈ 𝐽 ∣ 𝜑}. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∃𝑠 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑠 ∧ ∀𝑦 ∈ 𝑠 𝜑))
Theorem	cmpcovf 23327*	Combine cmpcov 23325 with ac6sfi 9290 to show the existence of a function that indexes the elements that are generating the open cover. (Contributed by Mario Carneiro, 14-Sep-2014.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝑧 = (𝑓‘𝑦) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝐴 𝜑)) → ∃𝑠 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑠 ∧ ∃𝑓(𝑓:𝑠⟶𝐴 ∧ ∀𝑦 ∈ 𝑠 𝜓)))
Theorem	cncmp 23328	Compactness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Comp)
Theorem	fincmp 23329	A finite topology is compact. (Contributed by FL, 22-Dec-2008.)
⊢ (𝐽 ∈ (Top ∩ Fin) → 𝐽 ∈ Comp)
Theorem	0cmp 23330	The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.)
⊢ {∅} ∈ Comp
Theorem	cmptop 23331	A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
Theorem	rncmp 23332	The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ↾t ran 𝐹) ∈ Comp)
Theorem	imacmp 23333	The image of a compact set under a continuous function is compact. (Contributed by Mario Carneiro, 18-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ (𝐽 ↾t 𝐴) ∈ Comp) → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Comp)
Theorem	discmp 23334	A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Comp)
Theorem	cmpsublem 23335*	Lemma for cmpsub 23336. (Contributed by Jeff Hankins, 28-Jun-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
Theorem	cmpsub 23336*	Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman's Beginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑)))
Theorem	tgcmp 23337*	A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23981, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
Theorem	cmpcld 23338	A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp)
Theorem	uncmp 23339	The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)
Theorem	fiuncmp 23340*	A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)
Theorem	sscmp 23341	A subset of a compact topology (i.e. a coarser topology) is compact. (Contributed by Mario Carneiro, 20-Mar-2015.)
⊢ 𝑋 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Comp ∧ 𝐽 ⊆ 𝐾) → 𝐽 ∈ Comp)
Theorem	hauscmplem 23342*	Lemma for hauscmp 23343. (Contributed by Mario Carneiro, 27-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}    &   ⊢ (𝜑 → 𝐽 ∈ Haus)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
Theorem	hauscmp 23343	A compact subspace of a T2 space is closed. (Contributed by Jeff Hankins, 16-Jan-2010.) (Proof shortened by Mario Carneiro, 14-Dec-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	cmpfi 23344*	If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
⊢ (𝐽 ∈ Top → (𝐽 ∈ Comp ↔ ∀𝑥 ∈ 𝒫 (Clsd‘𝐽)(¬ ∅ ∈ (fi‘𝑥) → ∩ 𝑥 ≠ ∅)))
Theorem	cmpfii 23345	In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝐽 ∈ Comp ∧ 𝑋 ⊆ (Clsd‘𝐽) ∧ ¬ ∅ ∈ (fi‘𝑋)) → ∩ 𝑋 ≠ ∅)
12.1.12  Bolzano-Weierstrass theorem
Theorem	bwth 23346*	The glorious Bolzano-Weierstrass theorem. The first general topology theorem ever proved. The first mention of this theorem can be found in a course by Weierstrass from 1865. In his course Weierstrass called it a lemma. He didn't know how famous this theorem would be. He used a Euclidean space instead of a general compact space. And he was not aware of the Heine-Borel property. But the concepts of neighborhood and limit point were already there although not precisely defined. Cantor was one of his students. He published and used the theorem in an article from 1872. The rest of the general topology followed from that. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) Revised by BL to significantly shorten the proof and avoid infinity, regularity, and choice. (Revised by Brendan Leahy, 26-Dec-2018.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴))
12.1.13  Connectedness
Syntax	cconn 23347	Extend class notation with the class of all connected topologies.
class Conn
Definition	df-conn 23348	Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.)
⊢ Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}}
Theorem	isconn 23349	The predicate 𝐽 is a connected topology . (Contributed by FL, 17-Nov-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) = {∅, 𝑋}))
Theorem	isconn2 23350	The predicate 𝐽 is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝑋}))
Theorem	connclo 23351	The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 = 𝑋)
Theorem	conndisj 23352	If a topology is connected, its underlying set can't be partitioned into two nonempty non-overlapping open sets. (Contributed by FL, 16-Nov-2008.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ≠ 𝑋)
Theorem	conntop 23353	A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.)
⊢ (𝐽 ∈ Conn → 𝐽 ∈ Top)
Theorem	indisconn 23354	The indiscrete topology (or trivial topology) on any set is connected. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, 𝐴} ∈ Conn
Theorem	dfconn2 23355*	An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))
Theorem	connsuba 23356*	Connectedness for a subspace. See connsub 23357. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐽 ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝐴) ≠ ∅ ∧ (𝑦 ∩ 𝐴) ≠ ∅ ∧ ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) → ((𝑥 ∪ 𝑦) ∩ 𝐴) ≠ 𝐴)))
Theorem	connsub 23357*	Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝑆) ≠ ∅ ∧ (𝑦 ∩ 𝑆) ≠ ∅ ∧ (𝑥 ∩ 𝑦) ⊆ (𝑋 ∖ 𝑆)) → ¬ 𝑆 ⊆ (𝑥 ∪ 𝑦))))
Theorem	cnconn 23358	Connectedness is respected by a continuous onto map. (Contributed by Jeff Hankins, 12-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ ((𝐽 ∈ Conn ∧ 𝐹:𝑋–onto→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Conn)
Theorem	nconnsubb 23359	Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑈 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → (𝑉 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → ((𝑈 ∩ 𝑉) ∩ 𝐴) = ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑈 ∪ 𝑉))    ⇒   ⊢ (𝜑 → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
Theorem	connsubclo 23360	If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Conn)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐽)    &   ⊢ (𝜑 → (𝐵 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
Theorem	connima 23361	The image of a connected set is connected. (Contributed by Mario Carneiro, 7-Jul-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝐴) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐾 ↾t (𝐹 “ 𝐴)) ∈ Conn)
Theorem	conncn 23362	A continuous function from a connected topology with one point in a clopen set must lie entirely within the set. (Contributed by Mario Carneiro, 16-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → 𝑈 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐾))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝐹‘𝐴) ∈ 𝑈)    ⇒   ⊢ (𝜑 → 𝐹:𝑋⟶𝑈)
Theorem	iunconnlem 23363*	Lemma for iunconn 23364. (Contributed by Mario Carneiro, 11-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅)    &   ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵))    &   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉))    &   ⊢ Ⅎ𝑘𝜑    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈)
Theorem	iunconn 23364*	The indexed union of connected overlapping subspaces sharing a common point is connected. (Contributed by Mario Carneiro, 11-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐽 ↾t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)
Theorem	unconn 23365	The union of two connected overlapping subspaces is connected. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 11-Jun-2014.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) ∧ (𝐴 ∩ 𝐵) ≠ ∅) → (((𝐽 ↾t 𝐴) ∈ Conn ∧ (𝐽 ↾t 𝐵) ∈ Conn) → (𝐽 ↾t (𝐴 ∪ 𝐵)) ∈ Conn))
Theorem	clsconn 23366	The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Conn) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Conn)
Theorem	conncompid 23367*	The connected component containing 𝐴 contains 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑆)
Theorem	conncompconn 23368*	The connected component containing 𝐴 is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
Theorem	conncompss 23369*	The connected component containing 𝐴 is a superset of any other connected set containing 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ (𝐽 ↾t 𝑇) ∈ Conn) → 𝑇 ⊆ 𝑆)
Theorem	conncompcld 23370*	The connected component containing 𝐴 is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	conncompclo 23371*	The connected component containing 𝐴 is a subset of any clopen set containing 𝐴. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑇 ∈ (𝐽 ∩ (Clsd‘𝐽)) ∧ 𝐴 ∈ 𝑇) → 𝑆 ⊆ 𝑇)
Theorem	t1connperf 23372	A connected T1 space is perfect, unless it is the topology of a singleton. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ∧ ¬ 𝑋 ≈ 1o) → 𝐽 ∈ Perf)
12.1.14  First- and second-countability
Syntax	c1stc 23373	Extend class definition to include the class of all first-countable topologies.
class 1stω
Syntax	c2ndc 23374	Extend class definition to include the class of all second-countable topologies.
class 2ndω
Definition	df-1stc 23375*	Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}
Definition	df-2ndc 23376*	Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.)
⊢ 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Theorem	is1stc 23377*	The predicate "is a first-countable topology." This can be described as "every point has a countable local basis" - that is, every point has a countable collection of open sets containing it such that every open set containing the point has an open set from this collection as a subset. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ 1stω ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))))
Theorem	is1stc2 23378*	An equivalent way of saying "is a first-countable topology." (Contributed by Jeff Hankins, 22-Aug-2009.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ 1stω ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝒫 𝐽(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝐽 (𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
Theorem	1stctop 23379	A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
Theorem	1stcclb 23380*	A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑧 ∈ 𝑥 (𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))
Theorem	1stcfb 23381*	For any point 𝐴 in a first-countable topology, there is a function 𝑓:ℕ⟶𝐽 enumerating neighborhoods of 𝐴 which is decreasing and forms a local base. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑓(𝑓:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ (𝐴 ∈ (𝑓‘𝑘) ∧ (𝑓‘(𝑘 + 1)) ⊆ (𝑓‘𝑘)) ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑘 ∈ ℕ (𝑓‘𝑘) ⊆ 𝑦)))
Theorem	is2ndc 23382*	The property of being second-countable. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 2ndω ↔ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝐽))
Theorem	2ndctop 23383	A second-countable topology is a topology. (Contributed by Jeff Hankins, 17-Jan-2010.) (Revised by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ Top)
Theorem	2ndci 23384	A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ≼ ω) → (topGen‘𝐵) ∈ 2ndω)
Theorem	2ndcsb 23385*	Having a countable subbase is a sufficient condition for second-countability. (Contributed by Jeff Hankins, 17-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ (𝐽 ∈ 2ndω ↔ ∃𝑥(𝑥 ≼ ω ∧ (topGen‘(fi‘𝑥)) = 𝐽))
Theorem	2ndcredom 23386	A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ≼ ℝ)
Theorem	2ndc1stc 23387	A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ 1stω)
Theorem	1stcrestlem 23388*	Lemma for 1stcrest 23389. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω)
Theorem	1stcrest 23389	A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 1stω)
Theorem	2ndcrest 23390	A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ 2ndω ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 2ndω)
Theorem	2ndcctbss 23391*	If a topology is second-countable, every base has a countable subset which is a base. Exercise 16B2 in Willard. (Contributed by Jeff Hankins, 28-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
⊢ 𝐽 = (topGen‘𝐵)    &   ⊢ 𝑆 = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))}    ⇒   ⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))
Theorem	2ndcdisj 23392*	Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
⊢ ((𝐽 ∈ 2ndω ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)
Theorem	2ndcdisj2 23393*	Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.)
⊢ ((𝐽 ∈ 2ndω ∧ 𝐴 ⊆ 𝐽 ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝑥) → 𝐴 ≼ ω)
Theorem	2ndcomap 23394*	A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑌 = ∪ 𝐾    &   ⊢ (𝜑 → 𝐽 ∈ 2ndω)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = 𝑌)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾)    ⇒   ⊢ (𝜑 → 𝐾 ∈ 2ndω)
Theorem	2ndcsep 23395*	A second-countable topology is separable, which is to say it contains a countable dense subset. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ 2ndω → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))
Theorem	dis2ndc 23396	A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω)
Theorem	1stcelcls 23397*	A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. This proof uses countable choice ax-cc 10447. A space satisfying the conclusion of this theorem is called a sequential space, so the theorem can also be stated as "every first-countable space is a sequential space". (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
Theorem	1stccnp 23398*	A mapping is continuous at 𝑃 in a first-countable space 𝑋 iff it is sequentially continuous at 𝑃, meaning that the image under 𝐹 of every sequence converging at 𝑃 converges to 𝐹(𝑃). This proof uses ax-cc 10447, but only via 1stcelcls 23397, so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ 1stω)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))))
Theorem	1stccn 23399*	A mapping 𝑋⟶𝑌, where 𝑋 is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence 𝑓(𝑛) converging to 𝑥, its image under 𝐹 converges to 𝐹(𝑥). (Contributed by Mario Carneiro, 7-Sep-2015.)
⊢ (𝜑 → 𝐽 ∈ 1stω)    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑓(𝑓:ℕ⟶𝑋 → ∀𝑥(𝑓(⇝𝑡‘𝐽)𝑥 → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑥)))))
12.1.15  Local topological properties
Syntax	clly 23400	Extend class notation with the "locally 𝐴 " predicate of a topological space.
class Locally 𝐴