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	tgdom 23301	A space has no more open sets than subsets of a basis. (Contributed by Stefan O'Rear, 22-Feb-2015.) (Revised by Mario Carneiro, 9-Apr-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ≼ 𝒫 𝐵)
Theorem	tgiun 23302*	The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ (topGen‘𝐵))
Theorem	tgidm 23303	The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))
Theorem	bastop 23304	Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))
Theorem	tgtop11 23305	The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾)
Theorem	0top 23306	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 23307	{∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅}))
Theorem	en2top 23308	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 23309	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 23310*	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 23311	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 23312*	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 23313	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 23314	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 23315	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 23316*	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 23317*	A version of bastop1 23316 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.)
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))))
12.1.3  Examples of topologies
Theorem	distop 23318	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 23319	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7773; an alternate proof uses indiscrete topologies (see indistop 23325) and the analogue of pwnex 7773 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7771). (Contributed by BJ, 2-May-2021.)
⊢ Top ∉ V
Theorem	distopon 23320	The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
Theorem	sn0topon 23321	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ {∅} ∈ (TopOn‘∅)
Theorem	sn0top 23322	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 23323	A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴}
Theorem	indistopon 23324	The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴))
Theorem	indistop 23325	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 23326	The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴}
Theorem	fctop 23327*	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 23328*	The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 23327 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	cctop 23329*	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 23330*	The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	pptbas 23331*	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 23332*	The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
Theorem	indistpsx 23333	The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 23334 and indistps2 23335. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17377 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 17393 and df-tset 17452 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 23334 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨1, 𝐴⟩, ⟨9, {∅, 𝐴}⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistps 23334	The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 23333 is that it is independent of the indices of the component definitions df-base 17393 and df-tset 17452, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 23335 is that it is easy to eliminate the hypotheses with eqid 2760 and vtoclg 3517 to result in a closed theorem. Theorems indistpsALT 23336 and indistps2ALT 23337 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 23335	The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 23334. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 23336 and indistps2ALT 23337 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistpsALT 23336	The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 23334 from the direct component assignment version indistps2 23335. (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 23337	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 23335 from the structural version indistps 23334. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	distps 23338	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 23339	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 23340	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 23341	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 23342*	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 23343*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 23359. (Contributed by NM, 10-Sep-2006.)
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
Definition	df-cls 23344*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 23360. (Contributed by NM, 3-Oct-2006.)
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))
Theorem	fncld 23345	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ Clsd Fn Top
Theorem	cldval 23346*	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 23347*	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 23348*	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 23349	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
Theorem	iscld 23350	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 23351	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 23352	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 23353	The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
Theorem	cldopn 23354	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 23355	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 23356	The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽))
Theorem	difopn 23357	The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽)
Theorem	topcld 23358	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 23359	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 23360*	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 23361	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 23362*	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 23363	The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∩ 𝐴 ∈ (Clsd‘𝐽))
Theorem	uncld 23364	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 23365	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆)
Theorem	incld 23366	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 23367*	An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ (Clsd‘𝐽))
Theorem	iuncld 23368*	A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽))
Theorem	unicld 23369	A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪ 𝐴 ∈ (Clsd‘𝐽))
Theorem	clscld 23370	The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
Theorem	clsf 23371	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 23372	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 23373	Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrval2 23374	Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrdif 23375	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 23376	A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((int‘𝐽)‘𝐴)))
Theorem	clsss 23377	Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss 23378	Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆))
Theorem	sscls 23379	A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss2 23380	A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)
Theorem	ssntr 23381	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 23382	The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrss3 23383	The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrin 23384	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 23385	The complement of a closure is open. (Contributed by NM, 11-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽)
Theorem	cmntrcld 23386	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 23387	A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆))
Theorem	iscld4 23388	A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) ⊆ 𝑆))
Theorem	isopn3 23389	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 23390	The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((cls‘𝐽)‘𝑆))
Theorem	ntridm 23391	The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆))
Theorem	clstop 23392	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 23393	The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋)
Theorem	0ntr 23394	A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (((𝐽 ∈ Top ∧ 𝑋 ≠ ∅) ∧ (𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘𝑆) = ∅)) → (𝑋 ∖ 𝑆) ≠ ∅)
Theorem	clsss2 23395	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 23396*	Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑃 ∈ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅)))
Theorem	elcls2 23397*	Membership in a closure. (Contributed by NM, 5-Mar-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ 𝐽 (𝑃 ∈ 𝑥 → (𝑥 ∩ 𝑆) ≠ ∅))))
Theorem	clsndisj 23398	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 23399	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 23400*	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‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥 ∈ 𝐽 (𝑥 ⊆ 𝑆 → 𝑥 = ∅)))