P. 222 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22101-22200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cldcls 22101	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆)
Theorem	incld 22102	The intersection of two closed sets is closed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∩ 𝐵) ∈ (Clsd‘𝐽))
Theorem	riincld 22103*	An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ (Clsd‘𝐽))
Theorem	iuncld 22104*	A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽))
Theorem	unicld 22105	A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪ 𝐴 ∈ (Clsd‘𝐽))
Theorem	clscld 22106	The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
Theorem	clsf 22107	The closure function is a function from subsets of the base to closed sets. (Contributed by Mario Carneiro, 11-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (cls‘𝐽):𝒫 𝑋⟶(Clsd‘𝐽))
Theorem	ntropn 22108	The interior of a subset of a topology's underlying set is open. (Contributed by NM, 11-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ∈ 𝐽)
Theorem	clsval2 22109	Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrval2 22110	Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrdif 22111	An interior of a complement is the complement of the closure. This set is also known as the exterior of 𝐴. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((int‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((cls‘𝐽)‘𝐴)))
Theorem	clsdif 22112	A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((int‘𝐽)‘𝐴)))
Theorem	clsss 22113	Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss 22114	Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆))
Theorem	sscls 22115	A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss2 22116	A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)
Theorem	ssntr 22117	An open subset of a set is a subset of the set's interior. (Contributed by Jeff Hankins, 31-Aug-2009.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆)) → 𝑂 ⊆ ((int‘𝐽)‘𝑆))
Theorem	clsss3 22118	The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrss3 22119	The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrin 22120	A pairwise intersection of interiors is the interior of the intersection. This does not always hold for arbitrary intersections. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((int‘𝐽)‘(𝐴 ∩ 𝐵)) = (((int‘𝐽)‘𝐴) ∩ ((int‘𝐽)‘𝐵)))
Theorem	cmclsopn 22121	The complement of a closure is open. (Contributed by NM, 11-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽)
Theorem	cmntrcld 22122	The complement of an interior is closed. (Contributed by NM, 1-Oct-2007.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((int‘𝐽)‘𝑆)) ∈ (Clsd‘𝐽))
Theorem	iscld3 22123	A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆))
Theorem	iscld4 22124	A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) ⊆ 𝑆))
Theorem	isopn3 22125	A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆))
Theorem	clsidm 22126	The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((cls‘𝐽)‘𝑆))
Theorem	ntridm 22127	The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆))
Theorem	clstop 22128	The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon, 11-Mar-2023.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋)
Theorem	ntrtop 22129	The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋)
Theorem	0ntr 22130	A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑋 ≠ ∅) ∧ (𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑆) = ∅)) → (𝑋 ∖ 𝑆) ≠ ∅)
Theorem	clsss2 22131	If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐶 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝐶) → ((cls‘𝐽)‘𝑆) ⊆ 𝐶)
Theorem	elcls 22132*	Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)))
Theorem	elcls2 22133*	Membership in a closure. (Contributed by NM, 5-Mar-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))))
Theorem	clsndisj 22134	Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ ((cls‘𝐽)‘𝑆)) ∧ (𝑈 ∈ 𝐽 ∧ 𝑃 ∈ 𝑈)) → (𝑈 ∩ 𝑆) ≠ ∅)
Theorem	ntrcls0 22135	A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑆)) = ∅) → ((int‘𝐽)‘𝑆) = ∅)
Theorem	ntreq0 22136*	Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((int‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥 ∈ 𝐽 (𝑥 ⊆ 𝑆 → 𝑥 = ∅)))
Theorem	cldmre 22137	The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ∈ (Moore‘𝑋))
Theorem	mrccls 22138	Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘(Clsd‘𝐽))    ⇒   ⊢ (𝐽 ∈ Top → (cls‘𝐽) = 𝐹)
Theorem	cls0 22139	The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.)
⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)
Theorem	ntr0 22140	The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) = ∅)
Theorem	isopn3i 22141	An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆)
Theorem	elcls3 22142*	Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ (𝜑 → 𝐽 = (topGen‘𝐵))    &   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)    &   ⊢ (𝜑 → 𝐵 ∈ TopBases)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐵 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)))
Theorem	opncldf1 22143*	A bijection useful for converting statements about open sets to statements about closed sets and vice versa. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐹 = (𝑢 ∈ 𝐽 ↦ (𝑋 ∖ 𝑢))    ⇒   ⊢ (𝐽 ∈ Top → (𝐹:𝐽–1-1-onto→(Clsd‘𝐽) ∧ ◡𝐹 = (𝑥 ∈ (Clsd‘𝐽) ↦ (𝑋 ∖ 𝑥))))
Theorem	opncldf2 22144*	The values of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐹 = (𝑢 ∈ 𝐽 ↦ (𝑋 ∖ 𝑢))    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → (𝐹‘𝐴) = (𝑋 ∖ 𝐴))
Theorem	opncldf3 22145*	The values of the converse/inverse of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝐹 = (𝑢 ∈ 𝐽 ↦ (𝑋 ∖ 𝑢))    ⇒   ⊢ (𝐵 ∈ (Clsd‘𝐽) → (◡𝐹‘𝐵) = (𝑋 ∖ 𝐵))
Theorem	isclo 22146*	A set 𝐴 is clopen iff for every point 𝑥 in the space there is a neighborhood 𝑦 such that all the points in 𝑦 are in 𝐴 iff 𝑥 is. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴))))
Theorem	isclo2 22147*	A set 𝐴 is clopen iff for every point 𝑥 in the space there is a neighborhood 𝑦 of 𝑥 which is either disjoint from 𝐴 or contained in 𝐴. (Contributed by Mario Carneiro, 7-Jul-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ (𝐽 ∩ (Clsd‘𝐽)) ↔ ∀𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 (𝑧 ∈ 𝐴 → 𝑦 ⊆ 𝐴))))
Theorem	discld 22148	The open sets of a discrete topology are closed and its closed sets are open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro, 7-Apr-2015.)
⊢ (𝐴 ∈ 𝑉 → (Clsd‘𝒫 𝐴) = 𝒫 𝐴)
Theorem	sn0cld 22149	The closed sets of the topology {∅}. (Contributed by FL, 5-Jan-2009.)
⊢ (Clsd‘{∅}) = {∅}
Theorem	indiscld 22150	The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.)
⊢ (Clsd‘{∅, 𝐴}) = {∅, 𝐴}
Theorem	mretopd 22151*	A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝜑 → 𝑀 ∈ (Moore‘𝐵))    &   ⊢ (𝜑 → ∅ ∈ 𝑀)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀 ∧ 𝑦 ∈ 𝑀) → (𝑥 ∪ 𝑦) ∈ 𝑀)    &   ⊢ 𝐽 = {𝑧 ∈ 𝒫 𝐵 ∣ (𝐵 ∖ 𝑧) ∈ 𝑀}    ⇒   ⊢ (𝜑 → (𝐽 ∈ (TopOn‘𝐵) ∧ 𝑀 = (Clsd‘𝐽)))
Theorem	toponmre 22152	The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 22053. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝐵 ∈ 𝑉 → (TopOn‘𝐵) ∈ (Moore‘𝒫 𝐵))
Theorem	cldmreon 22153	The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → (Clsd‘𝐽) ∈ (Moore‘𝐵))
Theorem	iscldtop 22154*	A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ (𝐾 ∈ (Clsd “ (TopOn‘𝐵)) ↔ (𝐾 ∈ (Moore‘𝐵) ∧ ∅ ∈ 𝐾 ∧ ∀𝑥 ∈ 𝐾 ∀𝑦 ∈ 𝐾 (𝑥 ∪ 𝑦) ∈ 𝐾))
Theorem	mreclatdemoBAD 22155	The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD 18196. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 7212 update): This proof uses the old df-clat 18132 and references the required instance of mreclatBAD 18196 as a hypothesis. When mreclatBAD 18196 is corrected to become mreclat, delete this theorem and uncomment the mreclatdemo below.
⊢ (((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊))) ∈ (Moore‘∪ (TopOpen‘𝑊)) → (toInc‘((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊)))) ∈ CLat)    ⇒   ⊢ (𝑊 ∈ (TopSp ∩ LMod) → (toInc‘((LSubSp‘𝑊) ∩ (Clsd‘(TopOpen‘𝑊)))) ∈ CLat)
12.1.5  Neighborhoods
Syntax	cnei 22156	Extend class notation with neighborhood relation for topologies.
class nei
Definition	df-nei 22157*	Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.)
⊢ nei = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∈ 𝒫 ∪ 𝑗 ∣ ∃𝑔 ∈ 𝑗 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑦)}))
Theorem	neifval 22158*	Value of the neighborhood function on the subsets of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (nei‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑥 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)}))
Theorem	neif 22159	The neighborhood function is a function from the set of the subsets of the base set of a topology. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (nei‘𝐽) Fn 𝒫 𝑋)
Theorem	neiss2 22160	A set with a neighborhood is a subset of the base set of a topology. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑋)
Theorem	neival 22161*	Value of the set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((nei‘𝐽)‘𝑆) = {𝑣 ∈ 𝒫 𝑋 ∣ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑣)})
Theorem	isnei 22162*	The predicate "the class 𝑁 is a neighborhood of 𝑆". (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁))))
Theorem	neiint 22163	An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ 𝑆 ⊆ ((int‘𝐽)‘𝑁)))
Theorem	isneip 22164*	The predicate "the class 𝑁 is a neighborhood of point 𝑃". (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝑋) → (𝑁 ∈ ((nei‘𝐽)‘{𝑃}) ↔ (𝑁 ⊆ 𝑋 ∧ ∃𝑔 ∈ 𝐽 (𝑃 ∈ 𝑔 ∧ 𝑔 ⊆ 𝑁))))
Theorem	neii1 22165	A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑁 ⊆ 𝑋)
Theorem	neisspw 22166	The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → ((nei‘𝐽)‘𝑆) ⊆ 𝒫 𝑋)
Theorem	neii2 22167*	Property of a neighborhood. (Contributed by NM, 12-Feb-2007.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑔 ∈ 𝐽 (𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ 𝑁))
Theorem	neiss 22168	Any neighborhood of a set 𝑆 is also a neighborhood of any subset 𝑅 ⊆ 𝑆. Similar to Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑅 ⊆ 𝑆) → 𝑁 ∈ ((nei‘𝐽)‘𝑅))
Theorem	ssnei 22169	A set is included in any of its neighborhoods. Generalization to subsets of elnei 22170. (Contributed by FL, 16-Nov-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → 𝑆 ⊆ 𝑁)
Theorem	elnei 22170	A point belongs to any of its neighborhoods. Property Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝑃 ∈ 𝐴 ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃})) → 𝑃 ∈ 𝑁)
Theorem	0nnei 22171	The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.)
⊢ ((𝐽 ∈ Top ∧ 𝑆 ≠ ∅) → ¬ ∅ ∈ ((nei‘𝐽)‘𝑆))
Theorem	neips 22172*	A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → (𝑁 ∈ ((nei‘𝐽)‘𝑆) ↔ ∀𝑝 ∈ 𝑆 𝑁 ∈ ((nei‘𝐽)‘{𝑝})))
Theorem	opnneissb 22173	An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆)))
Theorem	opnssneib 22174	Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽 ∧ 𝑁 ⊆ 𝑋) → (𝑆 ⊆ 𝑁 ↔ 𝑁 ∈ ((nei‘𝐽)‘𝑆)))
Theorem	ssnei2 22175	Any subset 𝑀 of 𝑋 containing a neighborhood 𝑁 of a set 𝑆 is a neighborhood of this set. Generalization to subsets of Property Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) ∧ (𝑁 ⊆ 𝑀 ∧ 𝑀 ⊆ 𝑋)) → 𝑀 ∈ ((nei‘𝐽)‘𝑆))
Theorem	neindisj 22176	Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑃 ∈ ((cls‘𝐽)‘𝑆) ∧ 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))) → (𝑁 ∩ 𝑆) ≠ ∅)
Theorem	opnneiss 22177	An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘𝑆))
Theorem	opnneip 22178	An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ 𝐽 ∧ 𝑃 ∈ 𝑁) → 𝑁 ∈ ((nei‘𝐽)‘{𝑃}))
Theorem	opnnei 22179*	A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009.)
⊢ (𝐽 ∈ Top → (𝑆 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝑆 𝑆 ∈ ((nei‘𝐽)‘{𝑥})))
Theorem	tpnei 22180	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 22177. (Contributed by FL, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (𝑆 ⊆ 𝑋 ↔ 𝑋 ∈ ((nei‘𝐽)‘𝑆)))
Theorem	neiuni 22181	The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑋 = ∪ ((nei‘𝐽)‘𝑆))
Theorem	neindisj2 22182*	A point 𝑃 belongs to the closure of a set 𝑆 iff every neighborhood of 𝑃 meets 𝑆. (Contributed by FL, 15-Sep-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝑃})(𝑛 ∩ 𝑆) ≠ ∅))
Theorem	topssnei 22183	A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.)
⊢ 𝑋 = ∪ 𝐽    &   ⊢ 𝑌 = ∪ 𝐾    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑋 = 𝑌) ∧ 𝐽 ⊆ 𝐾) → ((nei‘𝐽)‘𝑆) ⊆ ((nei‘𝐾)‘𝑆))
Theorem	innei 22184	The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆) ∧ 𝑀 ∈ ((nei‘𝐽)‘𝑆)) → (𝑁 ∩ 𝑀) ∈ ((nei‘𝐽)‘𝑆))
Theorem	opnneiid 22185	Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.)
⊢ (𝐽 ∈ Top → (𝑁 ∈ ((nei‘𝐽)‘𝑁) ↔ 𝑁 ∈ 𝐽))
Theorem	neissex 22186*	For any neighborhood 𝑁 of 𝑆, there is a neighborhood 𝑥 of 𝑆 such that 𝑁 is a neighborhood of all subsets of 𝑥. Generalization to subsets of Property Viv of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝑆)) → ∃𝑥 ∈ ((nei‘𝐽)‘𝑆)∀𝑦(𝑦 ⊆ 𝑥 → 𝑁 ∈ ((nei‘𝐽)‘𝑦)))
Theorem	0nei 22187	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
⊢ (𝐽 ∈ Top → ∅ ∈ ((nei‘𝐽)‘∅))
Theorem	neipeltop 22188*	Lemma for neiptopreu 22192. (Contributed by Thierry Arnoux, 6-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    ⇒   ⊢ (𝐶 ∈ 𝐽 ↔ (𝐶 ⊆ 𝑋 ∧ ∀𝑝 ∈ 𝐶 𝐶 ∈ (𝑁‘𝑝)))
Theorem	neiptopuni 22189*	Lemma for neiptopreu 22192. (Contributed by Thierry Arnoux, 6-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
Theorem	neiptoptop 22190*	Lemma for neiptopreu 22192. (Contributed by Thierry Arnoux, 7-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → 𝐽 ∈ Top)
Theorem	neiptopnei 22191*	Lemma for neiptopreu 22192. (Contributed by Thierry Arnoux, 7-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐽)‘{𝑝})))
Theorem	neiptopreu 22192*	If, to each element 𝑃 of a set 𝑋, we associate a set (𝑁‘𝑃) fulfilling Properties Vi, Vii, Viii and Property Viv of [BourbakiTop1] p. I.2. , corresponding to ssnei 22169, innei 22184, elnei 22170 and neissex 22186, then there is a unique topology 𝑗 such that for any point 𝑝, (𝑁‘𝑝) is the set of neighborhoods of 𝑝. Proposition 2 of [BourbakiTop1] p. I.3. This can be used to build a topology from a set of neighborhoods. Note that innei 22184 uses binary intersections whereas Property Vii mentions finite intersections (which includes the empty intersection of subsets of 𝑋, which is equal to 𝑋), so we add the hypothesis that 𝑋 is a neighborhood of all points. TODO: when df-fi 9100 includes the empty intersection, remove that extra hypothesis. (Contributed by Thierry Arnoux, 6-Jan-2018.)
⊢ 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}    &   ⊢ (𝜑 → 𝑁:𝑋⟶𝒫 𝒫 𝑋)    &   ⊢ ((((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝))    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎)    &   ⊢ (((𝜑 ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞))    &   ⊢ ((𝜑 ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝))    ⇒   ⊢ (𝜑 → ∃!𝑗 ∈ (TopOn‘𝑋)𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝑗)‘{𝑝})))
12.1.6  Limit points and perfect sets
Syntax	clp 22193	Extend class notation with the limit point function for topologies.
class limPt
Syntax	cperf 22194	Extend class notation with the class of all perfect spaces.
class Perf
Definition	df-lp 22195*	Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 22198. (Contributed by NM, 10-Feb-2007.)
⊢ limPt = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝑗)‘(𝑥 ∖ {𝑦}))}))
Definition	df-perf 22196	Define the class of all perfect spaces. A perfect space is one for which every point in the set is a limit point of the whole space. (Contributed by Mario Carneiro, 24-Dec-2016.)
⊢ Perf = {𝑗 ∈ Top ∣ ((limPt‘𝑗)‘∪ 𝑗) = ∪ 𝑗}
Theorem	lpfval 22197*	The limit point function on the subsets of a topology's base set. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (limPt‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ {𝑦 ∣ 𝑦 ∈ ((cls‘𝐽)‘(𝑥 ∖ {𝑦}))}))
Theorem	lpval 22198*	The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in [Munkres] p. 97. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) = {𝑥 ∣ 𝑥 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑥}))})
Theorem	islp 22199	The predicate "the class 𝑃 is a limit point of 𝑆". (Contributed by NM, 10-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((limPt‘𝐽)‘𝑆) ↔ 𝑃 ∈ ((cls‘𝐽)‘(𝑆 ∖ {𝑃}))))
Theorem	lpsscls 22200	The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘𝑆) ⊆ ((cls‘𝐽)‘𝑆))