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	0top 23101	The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006.)
⊢ (𝐽 ∈ Top → (∪ 𝐽 = ∅ ↔ 𝐽 = {∅}))
Theorem	en1top 23102	{∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅}))
Theorem	en2top 23103	If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2o ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)))
Theorem	tgss3 23104	A criterion for determining whether one topology is finer than another. Lemma 2.2 of [Munkres] p. 80 using abbreviations. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((topGen‘𝐵) ⊆ (topGen‘𝐶) ↔ 𝐵 ⊆ (topGen‘𝐶)))
Theorem	tgss2 23105*	A criterion for determining whether one topology is finer than another, based on a comparison of their bases. Lemma 2.2 of [Munkres] p. 80. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪ 𝐶) → ((topGen‘𝐵) ⊆ (topGen‘𝐶) ↔ ∀𝑥 ∈ ∪ 𝐵∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝐶 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))))
Theorem	basgen 23106	Given a topology 𝐽, show that a subset 𝐵 satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81 using abbreviations. (Contributed by NM, 22-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐽)
Theorem	basgen2 23107*	Given a topology 𝐽, show that a subset 𝐵 satisfying the third antecedent is a basis for it. Lemma 2.3 of [Munkres] p. 81. (Contributed by NM, 20-Jul-2006.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) → (topGen‘𝐵) = 𝐽)
Theorem	2basgen 23108	Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = (topGen‘𝐶))
Theorem	tgfiss 23109	If a subbase is included into a topology, so is the generated topology. (Contributed by FL, 20-Apr-2012.) (Proof shortened by Mario Carneiro, 10-Jan-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → (topGen‘(fi‘𝐴)) ⊆ 𝐽)
Theorem	tgdif0 23110	A generated topology is not affected by the addition or removal of the empty set from the base. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ (topGen‘(𝐵 ∖ {∅})) = (topGen‘𝐵)
Theorem	bastop1 23111*	A subset of a topology is a basis for the topology iff every member of the topology is a union of members of the basis. We use the idiom "(topGen‘𝐵) = 𝐽 " to express "𝐵 is a basis for topology 𝐽 " since we do not have a separate notation for this. Definition 15.35 of [Schechter] p. 428. (Contributed by NM, 2-Feb-2008.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽) → ((topGen‘𝐵) = 𝐽 ↔ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))
Theorem	bastop2 23112*	A version of bastop1 23111 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.)
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))))
12.1.3  Examples of topologies
Theorem	distop 23113	The discrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro, 19-Mar-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top)
Theorem	topnex 23114	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7746; an alternate proof uses indiscrete topologies (see indistop 23120) and the analogue of pwnex 7746 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7744). (Contributed by BJ, 2-May-2021.)
⊢ Top ∉ V
Theorem	distopon 23115	The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
Theorem	sn0topon 23116	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ {∅} ∈ (TopOn‘∅)
Theorem	sn0top 23117	The singleton of the empty set is a topology. (Contributed by Stefan Allan, 3-Mar-2006.) (Proof shortened by Mario Carneiro, 13-Aug-2015.)
⊢ {∅} ∈ Top
Theorem	indislem 23118	A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴}
Theorem	indistopon 23119	The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴))
Theorem	indistop 23120	The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 16-Jul-2006.) (Revised by Stefan Allan, 6-Nov-2008.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ {∅, 𝐴} ∈ Top
Theorem	indisuni 23121	The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴}
Theorem	fctop 23122*	The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	fctop2 23123*	The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 23122 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	cctop 23124*	The countable complement topology on a set 𝐴. Example 4 in [Munkres] p. 77. (Contributed by FL, 23-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≼ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	ppttop 23125*	The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	pptbas 23126*	The particular point topology is generated by a basis consisting of pairs {𝑥, 𝑃} for each 𝑥 ∈ 𝐴. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} = (topGen‘ran (𝑥 ∈ 𝐴 ↦ {𝑥, 𝑃})))
Theorem	epttop 23127*	The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
Theorem	indistpsx 23128	The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 23129 and indistps2 23130. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17244 is not needed, nor any other special definition outside of basic set theory. The disadvantage is that if the indices of the component definitions df-base 17260 and df-tset 17319 are changed in the future, this theorem will also have to be changed. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use indistps 23129 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨1, 𝐴⟩, ⟨9, {∅, 𝐴}⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistps 23129	The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 23128 is that it is independent of the indices of the component definitions df-base 17260 and df-tset 17319, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 23130 is that it is easy to eliminate the hypotheses with eqid 2765 and vtoclg 3525 to result in a closed theorem. Theorems indistpsALT 23131 and indistps2ALT 23132 show that the two forms can be derived from each other. (Contributed by FL, 19-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), {∅, 𝐴}⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistps2 23130	The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 23129. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 23131 and indistps2ALT 23132 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistpsALT 23131	The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 23129 from the direct component assignment version indistps2 23130. (Contributed by NM, 24-Oct-2012.) (Revised by AV, 31-Oct-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), {∅, 𝐴}⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistps2ALT 23132	The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Here we show how to derive the direct component assignment version indistps2 23130 from the structural version indistps 23129. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	distps 23133	The discrete topology on a set 𝐴 expressed as a topological space. (Contributed by FL, 20-Aug-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝒫 𝐴⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
12.1.4  Closure and interior
Syntax	ccld 23134	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 23135	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 23136	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 23137*	Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006.)
⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗 ∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗})
Definition	df-ntr 23138*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 23154. (Contributed by NM, 10-Sep-2006.)
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
Definition	df-cls 23139*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 23155. (Contributed by NM, 3-Oct-2006.)
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))
Theorem	fncld 23140	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ Clsd Fn Top
Theorem	cldval 23141*	The set of closed sets of a topology. (Note that the set of open sets is just the topology itself, so we don't have a separate definition.) (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽})
Theorem	ntrfval 23142*	The interior function on the subsets of a topology's base set. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (int‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∪ (𝐽 ∩ 𝒫 𝑥)))
Theorem	clsfval 23143*	The closure function on the subsets of a topology's base set. (Contributed by NM, 3-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (cls‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∩ {𝑦 ∈ (Clsd‘𝐽) ∣ 𝑥 ⊆ 𝑦}))
Theorem	cldrcl 23144	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
Theorem	iscld 23145	The predicate "the class 𝑆 is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽)))
Theorem	iscld2 23146	A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑆) ∈ 𝐽))
Theorem	cldss 23147	A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋)
Theorem	cldss2 23148	The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
Theorem	cldopn 23149	The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽)
Theorem	isopn2 23150	A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽)))
Theorem	opncld 23151	The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽))
Theorem	difopn 23152	The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽)
Theorem	topcld 23153	The underlying set of a topology is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 3-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
Theorem	ntrval 23154	The interior of a subset of a topology's base set is the union of all the open sets it includes. Definition of interior of [Munkres] p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆))
Theorem	clsval 23155*	The closure of a subset of a topology's base set is the intersection of all the closed sets that include it. Definition of closure of [Munkres] p. 94. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥})
Theorem	0cld 23156	The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.)
⊢ (𝐽 ∈ Top → ∅ ∈ (Clsd‘𝐽))
Theorem	iincld 23157*	The indexed intersection of a collection 𝐵(𝑥) of closed sets is closed. Theorem 6.1(2) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.) (Revised by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽))
Theorem	intcld 23158	The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∩ 𝐴 ∈ (Clsd‘𝐽))
Theorem	uncld 23159	The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.)
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∪ 𝐵) ∈ (Clsd‘𝐽))
Theorem	cldcls 23160	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆)
Theorem	incld 23161	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 23162*	An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ (Clsd‘𝐽))
Theorem	iuncld 23163*	A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽))
Theorem	unicld 23164	A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪ 𝐴 ∈ (Clsd‘𝐽))
Theorem	clscld 23165	The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
Theorem	clsf 23166	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 23167	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 23168	Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrval2 23169	Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrdif 23170	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 23171	A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((int‘𝐽)‘𝐴)))
Theorem	clsss 23172	Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss 23173	Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆))
Theorem	sscls 23174	A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss2 23175	A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)
Theorem	ssntr 23176	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 23177	The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrss3 23178	The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrin 23179	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 23180	The complement of a closure is open. (Contributed by NM, 11-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽)
Theorem	cmntrcld 23181	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 23182	A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆))
Theorem	iscld4 23183	A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) ⊆ 𝑆))
Theorem	isopn3 23184	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 23185	The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((cls‘𝐽)‘𝑆))
Theorem	ntridm 23186	The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆))
Theorem	clstop 23187	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 23188	The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋)
Theorem	0ntr 23189	A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑋 ≠ ∅) ∧ (𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑆) = ∅)) → (𝑋 ∖ 𝑆) ≠ ∅)
Theorem	clsss2 23190	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 23191*	Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)))
Theorem	elcls2 23192*	Membership in a closure. (Contributed by NM, 5-Mar-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))))
Theorem	clsndisj 23193	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 23194	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 23195*	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 23196	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 23197	Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015.)
⊢ 𝐹 = (mrCls‘(Clsd‘𝐽))    ⇒   ⊢ (𝐽 ∈ Top → (cls‘𝐽) = 𝐹)
Theorem	cls0 23198	The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.)
⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) = ∅)
Theorem	ntr0 23199	The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
⊢ (𝐽 ∈ Top → ((int‘𝐽)‘∅) = ∅)
Theorem	isopn3i 23200	An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.)
⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → ((int‘𝐽)‘𝑆) = 𝑆)