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	ist0-3 23301*	The predicate "is a T0 space" expressed in more familiar terms. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑜 ∈ 𝐽 ((𝑥 ∈ 𝑜 ∧ ¬ 𝑦 ∈ 𝑜) ∨ (¬ 𝑥 ∈ 𝑜 ∧ 𝑦 ∈ 𝑜)))))
Theorem	cnt0 23302	The preimage of a T0 topology under an injective map is T0. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐾 ∈ Kol2 ∧ 𝐹:𝑋–1-1→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Kol2)
Theorem	ist1-2 23303*	An alternate characterization of T1 spaces. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Fre ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (∀𝑜 ∈ 𝐽 (𝑥 ∈ 𝑜 → 𝑦 ∈ 𝑜) → 𝑥 = 𝑦)))
Theorem	t1t0 23304	A T1 space is a T0 space. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ (𝐽 ∈ Fre → 𝐽 ∈ Kol2)
Theorem	ist1-3 23305*	A space is T1 iff every point is the only point in the intersection of all open sets containing that point. (Contributed by Jeff Hankins, 31-Jan-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Fre ↔ ∀𝑥 ∈ 𝑋 ∩ {𝑜 ∈ 𝐽 ∣ 𝑥 ∈ 𝑜} = {𝑥}))
Theorem	cnt1 23306	The preimage of a T1 topology under an injective map is T1. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐾 ∈ Fre ∧ 𝐹:𝑋–1-1→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Fre)
Theorem	ishaus2 23307*	Express the predicate "𝐽 is a Hausdorff space." (Contributed by NM, 8-Mar-2007.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑛 ∈ 𝐽 ∃𝑚 ∈ 𝐽 (𝑥 ∈ 𝑛 ∧ 𝑦 ∈ 𝑚 ∧ (𝑛 ∩ 𝑚) = ∅))))
Theorem	haust1 23308	A Hausdorff space is a T1 space. (Contributed by FL, 11-Jun-2007.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Fre)
Theorem	hausnei2 23309*	The Hausdorff condition still holds if one considers general neighborhoods instead of open sets. (Contributed by Jeff Hankins, 5-Sep-2009.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Haus ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥 ≠ 𝑦 → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑥})∃𝑣 ∈ ((nei‘𝐽)‘{𝑦})(𝑢 ∩ 𝑣) = ∅)))
Theorem	cnhaus 23310	The preimage of a Hausdorff topology under an injective map is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐾 ∈ Haus ∧ 𝐹:𝑋–1-1→𝑌 ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Haus)
Theorem	nrmsep3 23311*	In a normal space, given a closed set 𝐵 inside an open set 𝐴, there is an open set 𝑥 such that 𝐵 ⊆ 𝑥 ⊆ cls(𝑥) ⊆ 𝐴. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐽 ∈ Nrm ∧ (𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽) ∧ 𝐵 ⊆ 𝐴)) → ∃𝑥 ∈ 𝐽 (𝐵 ⊆ 𝑥 ∧ ((cls‘𝐽)‘𝑥) ⊆ 𝐴))
Theorem	nrmsep2 23312*	In a normal space, any two disjoint closed sets have the property that each one is a subset of an open set whose closure is disjoint from the other. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.)
⊢ ((𝐽 ∈ Nrm ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐷 ∈ (Clsd‘𝐽) ∧ (𝐶 ∩ 𝐷) = ∅)) → ∃𝑥 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ (((cls‘𝐽)‘𝑥) ∩ 𝐷) = ∅))
Theorem	nrmsep 23313*	In a normal space, disjoint closed sets are separated by open sets. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ ((𝐽 ∈ Nrm ∧ (𝐶 ∈ (Clsd‘𝐽) ∧ 𝐷 ∈ (Clsd‘𝐽) ∧ (𝐶 ∩ 𝐷) = ∅)) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))
Theorem	isnrm2 23314*	An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma. (Contributed by Jeff Hankins, 1-Feb-2010.) (Proof shortened by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑑 ∈ (Clsd‘𝐽)((𝑐 ∩ 𝑑) = ∅ → ∃𝑜 ∈ 𝐽 (𝑐 ⊆ 𝑜 ∧ (((cls‘𝐽)‘𝑜) ∩ 𝑑) = ∅))))
Theorem	isnrm3 23315*	A topological space is normal iff any two disjoint closed sets are separated by open sets. (Contributed by Mario Carneiro, 24-Aug-2015.)
⊢ (𝐽 ∈ Nrm ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ (Clsd‘𝐽)∀𝑑 ∈ (Clsd‘𝐽)((𝑐 ∩ 𝑑) = ∅ → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))))
Theorem	cnrmi 23316	A subspace of a completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Nrm)
Theorem	cnrmnrm 23317	A completely normal space is normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ (𝐽 ∈ CNrm → 𝐽 ∈ Nrm)
Theorem	restcnrm 23318	A subspace of a completely normal space is completely normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐽 ∈ CNrm ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ CNrm)
Theorem	resthauslem 23319	Lemma for resthaus 23324 and similar theorems. If the topological property 𝐴 is preserved under injective preimages, then property 𝐴 passes to subspaces. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top)    &   ⊢ ((𝐽 ∈ 𝐴 ∧ ( I ↾ (𝑆 ∩ ∪ 𝐽)):(𝑆 ∩ ∪ 𝐽)–1-1→(𝑆 ∩ ∪ 𝐽) ∧ ( I ↾ (𝑆 ∩ ∪ 𝐽)) ∈ ((𝐽 ↾t 𝑆) Cn 𝐽)) → (𝐽 ↾t 𝑆) ∈ 𝐴)    ⇒   ⊢ ((𝐽 ∈ 𝐴 ∧ 𝑆 ∈ 𝑉) → (𝐽 ↾t 𝑆) ∈ 𝐴)
Theorem	lpcls 23320	The limit points of the closure of a subset are the same as the limit points of the set in a T1 space. (Contributed by Mario Carneiro, 26-Dec-2016.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((limPt‘𝐽)‘𝑆))
Theorem	perfcls 23321	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 23322	A subspace of a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Kol2 ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Kol2)
Theorem	restt1 23323	A subspace of a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ Fre)
Theorem	resthaus 23324	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 23325*	Any two points in a T1 space which have no separation are equal. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → 𝐵 ∈ 𝑜) → 𝐴 = 𝐵))
Theorem	t1sep 23326*	Any two distinct points in a T1 space are separated by an open set. (Contributed by Jeff Hankins, 1-Feb-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ≠ 𝐵)) → ∃𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 ∧ ¬ 𝐵 ∈ 𝑜))
Theorem	sncld 23327	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 23328	Lemma for sshaus 23331 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 23329	A topology finer than a T0 topology is T0. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Kol2 ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Kol2)
Theorem	sst1 23330	A topology finer than a T1 topology is T1. (Contributed by Mario Carneiro, 25-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Fre ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Fre)
Theorem	sshaus 23331	A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Haus ∧ 𝐾 ∈ (TopOn‘𝑋) ∧ 𝐽 ⊆ 𝐾) → 𝐾 ∈ Haus)
Theorem	regsep2 23332*	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 23333*	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 23334	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 7010). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐾 ∈ Fre ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ (◡𝐹 “ {𝑃}) ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐹:𝑋⟶{𝑃})
Theorem	ordtt1 23335	The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ Fre)
Theorem	lmmo 23336	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 23337	The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ (𝐽 ∈ Haus → Fun (⇝𝑡‘𝐽))
Theorem	dishaus 23338	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 23339*	Lemma for ordthaus 23340. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → (𝐴 ≠ 𝐵 → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))))
Theorem	ordthaus 23340	The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → (ordTop‘𝑅) ∈ Haus)
Theorem	xrhaus 23341	The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ (ordTop‘ ≤ ) ∈ Haus
12.1.11  Compactness
Syntax	ccmp 23342	Extend class notation with the class of all compact spaces.
class Comp
Definition	df-cmp 23343*	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 23344*	The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
Theorem	cmpcov 23345*	An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆) → ∃𝑠 ∈ (𝒫 𝑆 ∩ Fin)𝑋 = ∪ 𝑠)
Theorem	cmpcov2 23346*	Rewrite cmpcov 23345 for the cover {𝑦 ∈ 𝐽 ∣ 𝜑}. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∃𝑠 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑠 ∧ ∀𝑦 ∈ 𝑠 𝜑))
Theorem	cmpcovf 23347*	Combine cmpcov 23345 with ac6sfi 9196 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 23348	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 23349	A finite topology is compact. (Contributed by FL, 22-Dec-2008.)
⊢ (𝐽 ∈ (Top ∩ Fin) → 𝐽 ∈ Comp)
Theorem	0cmp 23350	The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.)
⊢ {∅} ∈ Comp
Theorem	cmptop 23351	A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
Theorem	rncmp 23352	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 23353	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 23354	A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Comp)
Theorem	cmpsublem 23355*	Lemma for cmpsub 23356. (Contributed by Jeff Hankins, 28-Jun-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
Theorem	cmpsub 23356*	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 23357*	A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 24001, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
Theorem	cmpcld 23358	A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp)
Theorem	uncmp 23359	The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)
Theorem	fiuncmp 23360*	A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)
Theorem	sscmp 23361	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 23362*	Lemma for hauscmp 23363. (Contributed by Mario Carneiro, 27-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}    &   ⊢ (𝜑 → 𝐽 ∈ Haus)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
Theorem	hauscmp 23363	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 23364*	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 23365	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 23366*	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 23367	Extend class notation with the class of all connected topologies.
class Conn
Definition	df-conn 23368	Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.)
⊢ Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}}
Theorem	isconn 23369	The predicate 𝐽 is a connected topology . (Contributed by FL, 17-Nov-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) = {∅, 𝑋}))
Theorem	isconn2 23370	The predicate 𝐽 is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝑋}))
Theorem	connclo 23371	The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 = 𝑋)
Theorem	conndisj 23372	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 23373	A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.)
⊢ (𝐽 ∈ Conn → 𝐽 ∈ Top)
Theorem	indisconn 23374	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 23375*	An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))
Theorem	connsuba 23376*	Connectedness for a subspace. See connsub 23377. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐽 ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝐴) ≠ ∅ ∧ (𝑦 ∩ 𝐴) ≠ ∅ ∧ ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) → ((𝑥 ∪ 𝑦) ∩ 𝐴) ≠ 𝐴)))
Theorem	connsub 23377*	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 23378	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 23379	Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑈 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → (𝑉 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → ((𝑈 ∩ 𝑉) ∩ 𝐴) = ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑈 ∪ 𝑉))    ⇒   ⊢ (𝜑 → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
Theorem	connsubclo 23380	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 23381	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 23382	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 23383*	Lemma for iunconn 23384. (Contributed by Mario Carneiro, 11-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅)    &   ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵))    &   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉))    &   ⊢ Ⅎ𝑘𝜑    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈)
Theorem	iunconn 23384*	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 23385	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 23386	The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Conn) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Conn)
Theorem	conncompid 23387*	The connected component containing 𝐴 contains 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑆)
Theorem	conncompconn 23388*	The connected component containing 𝐴 is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
Theorem	conncompss 23389*	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 23390*	The connected component containing 𝐴 is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	conncompclo 23391*	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 23392	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 23393	Extend class definition to include the class of all first-countable topologies.
class 1stω
Syntax	c2ndc 23394	Extend class definition to include the class of all second-countable topologies.
class 2ndω
Definition	df-1stc 23395*	Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}
Definition	df-2ndc 23396*	Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.)
⊢ 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Theorem	is1stc 23397*	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 23398*	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 23399	A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
Theorem	1stcclb 23400*	A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑧 ∈ 𝑥 (𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))