P. 232 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23101-23200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isreg2 23101*	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 23102	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 7056). (Contributed by NM, 15-Mar-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐾 ∈ Fre ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ (𝑃 ∈ 𝑌 ∧ 𝐴 ⊆ (◡𝐹 “ {𝑃}) ∧ ((cls‘𝐽)‘𝐴) = 𝑋)) → 𝐹:𝑋⟶{𝑃})
Theorem	ordtt1 23103	The order topology is T1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ (𝑅 ∈ PosetRel → (ordTop‘𝑅) ∈ Fre)
Theorem	lmmo 23104	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 23105	The convergence relation is function-like in a Hausdorff space. (Contributed by Mario Carneiro, 26-Dec-2013.)
⊢ (𝐽 ∈ Haus → Fun (⇝𝑡‘𝐽))
Theorem	dishaus 23106	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 23107*	Lemma for ordthaus 23108. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ 𝑋 = dom 𝑅    ⇒   ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → (𝐴 ≠ 𝐵 → ∃𝑚 ∈ (ordTop‘𝑅)∃𝑛 ∈ (ordTop‘𝑅)(𝐴 ∈ 𝑚 ∧ 𝐵 ∈ 𝑛 ∧ (𝑚 ∩ 𝑛) = ∅))))
Theorem	ordthaus 23108	The order topology of a total order is Hausdorff. (Contributed by Mario Carneiro, 13-Sep-2015.)
⊢ (𝑅 ∈ TosetRel → (ordTop‘𝑅) ∈ Haus)
Theorem	xrhaus 23109	The topology of the extended reals is Hausdorff. (Contributed by Thierry Arnoux, 24-Mar-2017.)
⊢ (ordTop‘ ≤ ) ∈ Haus
12.1.11  Compactness
Syntax	ccmp 23110	Extend class notation with the class of all compact spaces.
class Comp
Definition	df-cmp 23111*	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 23112*	The predicate "is a compact topology". (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 11-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
Theorem	cmpcov 23113*	An open cover of a compact topology has a finite subcover. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ 𝑆 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑆) → ∃𝑠 ∈ (𝒫 𝑆 ∩ Fin)𝑋 = ∪ 𝑠)
Theorem	cmpcov2 23114*	Rewrite cmpcov 23113 for the cover {𝑦 ∈ 𝐽 ∣ 𝜑}. (Contributed by Mario Carneiro, 11-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝜑)) → ∃𝑠 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑠 ∧ ∀𝑦 ∈ 𝑠 𝜑))
Theorem	cmpcovf 23115*	Combine cmpcov 23113 with ac6sfi 9289 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 23116	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 23117	A finite topology is compact. (Contributed by FL, 22-Dec-2008.)
⊢ (𝐽 ∈ (Top ∩ Fin) → 𝐽 ∈ Comp)
Theorem	0cmp 23118	The singleton of the empty set is compact. (Contributed by FL, 2-Aug-2009.)
⊢ {∅} ∈ Comp
Theorem	cmptop 23119	A compact topology is a topology. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
Theorem	rncmp 23120	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 23121	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 23122	A discrete topology is compact iff the base set is finite. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Comp)
Theorem	cmpsublem 23123*	Lemma for cmpsub 23124. (Contributed by Jeff Hankins, 28-Jun-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (∀𝑐 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑆 ⊆ ∪ 𝑑) → ∀𝑠 ∈ 𝒫 (𝐽 ↾t 𝑆)(∪ (𝐽 ↾t 𝑆) = ∪ 𝑠 → ∃𝑡 ∈ (𝒫 𝑠 ∩ Fin)∪ (𝐽 ↾t 𝑆) = ∪ 𝑡)))
Theorem	cmpsub 23124*	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 23125*	A topology generated by a basis is compact iff open covers drawn from the basis have finite subcovers. (See also alexsub 23769, which further specializes to subbases, assuming the ultrafilter lemma.) (Contributed by Mario Carneiro, 26-Aug-2015.)
⊢ ((𝐵 ∈ TopBases ∧ 𝑋 = ∪ 𝐵) → ((topGen‘𝐵) ∈ Comp ↔ ∀𝑦 ∈ 𝒫 𝐵(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)))
Theorem	cmpcld 23126	A closed subset of a compact space is compact. (Contributed by Jeff Hankins, 29-Jun-2009.)
⊢ ((𝐽 ∈ Comp ∧ 𝑆 ∈ (Clsd‘𝐽)) → (𝐽 ↾t 𝑆) ∈ Comp)
Theorem	uncmp 23127	The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑋 = (𝑆 ∪ 𝑇)) ∧ ((𝐽 ↾t 𝑆) ∈ Comp ∧ (𝐽 ↾t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)
Theorem	fiuncmp 23128*	A finite union of compact sets is compact. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 (𝐽 ↾t 𝐵) ∈ Comp) → (𝐽 ↾t ∪ 𝑥 ∈ 𝐴 𝐵) ∈ Comp)
Theorem	sscmp 23129	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 23130*	Lemma for hauscmp 23131. (Contributed by Mario Carneiro, 27-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}    &   ⊢ (𝜑 → 𝐽 ∈ Haus)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp)    &   ⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆))    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)))
Theorem	hauscmp 23131	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 23132*	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 23133	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 23134*	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 23135	Extend class notation with the class of all connected topologies.
class Conn
Definition	df-conn 23136	Topologies are connected when only ∅ and ∪ 𝑗 are both open and closed. (Contributed by FL, 17-Nov-2008.)
⊢ Conn = {𝑗 ∈ Top ∣ (𝑗 ∩ (Clsd‘𝑗)) = {∅, ∪ 𝑗}}
Theorem	isconn 23137	The predicate 𝐽 is a connected topology . (Contributed by FL, 17-Nov-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) = {∅, 𝑋}))
Theorem	isconn2 23138	The predicate 𝐽 is a connected topology . (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Conn ↔ (𝐽 ∈ Top ∧ (𝐽 ∩ (Clsd‘𝐽)) ⊆ {∅, 𝑋}))
Theorem	connclo 23139	The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ (𝜑 → 𝐽 ∈ Conn)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐽)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    &   ⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 = 𝑋)
Theorem	conndisj 23140	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 23141	A connected topology is a topology. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 14-Dec-2013.)
⊢ (𝐽 ∈ Conn → 𝐽 ∈ Top)
Theorem	indisconn 23142	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 23143*	An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 ((𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ (𝑥 ∩ 𝑦) = ∅) → (𝑥 ∪ 𝑦) ≠ 𝑋)))
Theorem	connsuba 23144*	Connectedness for a subspace. See connsub 23145. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ((𝐽 ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (((𝑥 ∩ 𝐴) ≠ ∅ ∧ (𝑦 ∩ 𝐴) ≠ ∅ ∧ ((𝑥 ∩ 𝑦) ∩ 𝐴) = ∅) → ((𝑥 ∪ 𝑦) ∩ 𝐴) ≠ 𝐴)))
Theorem	connsub 23145*	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 23146	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 23147	Disconnectedness for a subspace. (Contributed by FL, 29-May-2014.) (Proof shortened by Mario Carneiro, 10-Mar-2015.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑈 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → (𝑉 ∩ 𝐴) ≠ ∅)    &   ⊢ (𝜑 → ((𝑈 ∩ 𝑉) ∩ 𝐴) = ∅)    &   ⊢ (𝜑 → 𝐴 ⊆ (𝑈 ∪ 𝑉))    ⇒   ⊢ (𝜑 → ¬ (𝐽 ↾t 𝐴) ∈ Conn)
Theorem	connsubclo 23148	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 23149	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 23150	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 23151*	Lemma for iunconn 23152. (Contributed by Mario Carneiro, 11-Jun-2014.)
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾t 𝐵) ∈ Conn)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐽)    &   ⊢ (𝜑 → 𝑉 ∈ 𝐽)    &   ⊢ (𝜑 → (𝑉 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅)    &   ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵))    &   ⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑈 ∪ 𝑉))    &   ⊢ Ⅎ𝑘𝜑    ⇒   ⊢ (𝜑 → ¬ 𝑃 ∈ 𝑈)
Theorem	iunconn 23152*	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 23153	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 23154	The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ (𝐽 ↾t 𝐴) ∈ Conn) → (𝐽 ↾t ((cls‘𝐽)‘𝐴)) ∈ Conn)
Theorem	conncompid 23155*	The connected component containing 𝐴 contains 𝐴. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ 𝑆)
Theorem	conncompconn 23156*	The connected component containing 𝐴 is connected. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → (𝐽 ↾t 𝑆) ∈ Conn)
Theorem	conncompss 23157*	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 23158*	The connected component containing 𝐴 is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015.)
⊢ 𝑆 = ∪ {𝑥 ∈ 𝒫 𝑋 ∣ (𝐴 ∈ 𝑥 ∧ (𝐽 ↾t 𝑥) ∈ Conn)}    ⇒   ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝑋) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	conncompclo 23159*	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 23160	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 23161	Extend class definition to include the class of all first-countable topologies.
class 1stω
Syntax	c2ndc 23162	Extend class definition to include the class of all second-countable topologies.
class 2ndω
Definition	df-1stc 23163*	Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 1stω = {𝑗 ∈ Top ∣ ∀𝑥 ∈ ∪ 𝑗∃𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧 ∈ 𝑗 (𝑥 ∈ 𝑧 → 𝑥 ∈ ∪ (𝑦 ∩ 𝒫 𝑧)))}
Definition	df-2ndc 23164*	Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.)
⊢ 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Theorem	is1stc 23165*	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 23166*	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 23167	A first-countable topology is a topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ (𝐽 ∈ 1stω → 𝐽 ∈ Top)
Theorem	1stcclb 23168*	A property of points in a first-countable topology. (Contributed by Jeff Hankins, 22-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑋) → ∃𝑥 ∈ 𝒫 𝐽(𝑥 ≼ ω ∧ ∀𝑦 ∈ 𝐽 (𝐴 ∈ 𝑦 → ∃𝑧 ∈ 𝑥 (𝐴 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))
Theorem	1stcfb 23169*	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 23170*	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 23171	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 23172	A countable basis generates a second-countable topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐵 ∈ TopBases ∧ 𝐵 ≼ ω) → (topGen‘𝐵) ∈ 2ndω)
Theorem	2ndcsb 23173*	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 23174	A second-countable space has at most the cardinality of the continuum. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ≼ ℝ)
Theorem	2ndc1stc 23175	A second-countable space is first-countable. (Contributed by Jeff Hankins, 17-Jan-2010.)
⊢ (𝐽 ∈ 2ndω → 𝐽 ∈ 1stω)
Theorem	1stcrestlem 23176*	Lemma for 1stcrest 23177. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ (𝐵 ≼ ω → ran (𝑥 ∈ 𝐵 ↦ 𝐶) ≼ ω)
Theorem	1stcrest 23177	A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ 1stω ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 1stω)
Theorem	2ndcrest 23178	A subspace of a second-countable space is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ ((𝐽 ∈ 2ndω ∧ 𝐴 ∈ 𝑉) → (𝐽 ↾t 𝐴) ∈ 2ndω)
Theorem	2ndcctbss 23179*	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 23180*	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 23181*	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 23182*	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 23183*	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 23184	A discrete space is second-countable iff it is countable. (Contributed by Mario Carneiro, 13-Apr-2015.)
⊢ (𝑋 ≼ ω ↔ 𝒫 𝑋 ∈ 2ndω)
Theorem	1stcelcls 23185*	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 10432. 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 23186*	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 10432, but only via 1stcelcls 23185, 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 23187*	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 23188	Extend class notation with the "locally 𝐴 " predicate of a topological space.
class Locally 𝐴
Syntax	cnlly 23189	Extend class notation with the "N-locally 𝐴 " predicate of a topological space.
class 𝑛-Locally 𝐴
Definition	df-lly 23190*	Define a space that is locally 𝐴, where 𝐴 is a topological property like "compact", "connected", or "path-connected". A topological space is locally 𝐴 if every neighborhood of a point contains an open subneighborhood that is 𝐴 in the subspace topology. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝑗 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝑗 ↾t 𝑢) ∈ 𝐴)}
Definition	df-nlly 23191*	Define a space that is n-locally 𝐴, where 𝐴 is a topological property like "compact", "connected", or "path-connected". A topological space is n-locally 𝐴 if every neighborhood of a point contains a subneighborhood that is 𝐴 in the subspace topology. The terminology "n-locally", where 'n' stands for "neighborhood", is not standard, although this is sometimes called "weakly locally 𝐴". The reason for the distinction is that some notions only make sense for arbitrary neighborhoods (such as "locally compact", which is actually 𝑛-Locally Comp in our terminology - open compact sets are not very useful), while others such as "locally connected" are strictly weaker notions if the neighborhoods are not required to be open. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ 𝑛-Locally 𝐴 = {𝑗 ∈ Top ∣ ∀𝑥 ∈ 𝑗 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝑗)‘{𝑦}) ∩ 𝒫 𝑥)(𝑗 ↾t 𝑢) ∈ 𝐴}
Theorem	islly 23192*	The property of being a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (𝐽 ∩ 𝒫 𝑥)(𝑦 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴)))
Theorem	isnlly 23193*	The property of being an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ (((nei‘𝐽)‘{𝑦}) ∩ 𝒫 𝑥)(𝐽 ↾t 𝑢) ∈ 𝐴))
Theorem	llyeq 23194	Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐴 = 𝐵 → Locally 𝐴 = Locally 𝐵)
Theorem	nllyeq 23195	Equality theorem for the Locally 𝐴 predicate. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵)
Theorem	llytop 23196	A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ Locally 𝐴 → 𝐽 ∈ Top)
Theorem	nllytop 23197	A locally 𝐴 space is a topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ (𝐽 ∈ 𝑛-Locally 𝐴 → 𝐽 ∈ Top)
Theorem	llyi 23198*	The property of a locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ 𝐽 (𝑢 ⊆ 𝑈 ∧ 𝑃 ∈ 𝑢 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴))
Theorem	nllyi 23199*	The property of an n-locally 𝐴 topological space. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑢 ∈ ((nei‘𝐽)‘{𝑃})(𝑢 ⊆ 𝑈 ∧ (𝐽 ↾t 𝑢) ∈ 𝐴))
Theorem	nlly2i 23200*	Eliminate the neighborhood symbol from nllyi 23199. (Contributed by Mario Carneiro, 2-Mar-2015.)
⊢ ((𝐽 ∈ 𝑛-Locally 𝐴 ∧ 𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈) → ∃𝑠 ∈ 𝒫 𝑈∃𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑠 ∧ (𝐽 ↾t 𝑠) ∈ 𝐴))