Type  Label  Description 
Statement 

Theorem  tpspropd 11901 
A topological space depends only on the base and topology components.
(Contributed by NM, 18Jul2006.) (Revised by Mario Carneiro,
13Aug2015.)

⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))
⇒ ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp)) 

Theorem  topontopn 11902 
Express the predicate "is a topological space." (Contributed by
Mario
Carneiro, 13Aug2015.)

⊢ 𝐴 = (Base‘𝐾)
& ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾)) 

Theorem  tsettps 11903 
If the topology component is already correctly truncated, then it forms
a topological space (with the topology extractor function coming out the
same as the component). (Contributed by Mario Carneiro,
13Aug2015.)

⊢ 𝐴 = (Base‘𝐾)
& ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) 

Theorem  istpsi 11904 
Properties that determine a topological space. (Contributed by NM,
20Oct2012.)

⊢ (Base‘𝐾) = 𝐴
& ⊢ (TopOpen‘𝐾) = 𝐽
& ⊢ 𝐴 = ∪ 𝐽 & ⊢ 𝐽 ∈
Top ⇒ ⊢ 𝐾 ∈ TopSp 

Theorem  eltpsg 11905 
Properties that determine a topological space from a construction (using
no explicit indices). (Contributed by Mario Carneiro, 13Aug2015.)

⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩,
⟨(TopSet‘ndx), 𝐽⟩} ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) 

Theorem  eltpsi 11906 
Properties that determine a topological space from a construction (using
no explicit indices). (Contributed by NM, 20Oct2012.) (Revised by
Mario Carneiro, 13Aug2015.)

⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩,
⟨(TopSet‘ndx), 𝐽⟩} & ⊢ 𝐴 = ∪
𝐽 & ⊢ 𝐽 ∈
Top ⇒ ⊢ 𝐾 ∈ TopSp 

6.1.2 Topological bases


Syntax  ctb 11907 
Syntax for the class of topological bases.

class TopBases 

Definition  dfbases 11908* 
Define the class of topological bases. Equivalent to definition of
basis in [Munkres] p. 78 (see isbasis2g 11910). Note that "bases" is the
plural of "basis". (Contributed by NM, 17Jul2006.)

⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪
(𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))} 

Theorem  isbasisg 11909* 
Express the predicate "the set 𝐵 is a basis for a topology".
(Contributed by NM, 17Jul2006.)

⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪
(𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) 

Theorem  isbasis2g 11910* 
Express the predicate "the set 𝐵 is a basis for a topology".
(Contributed by NM, 17Jul2006.)

⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))) 

Theorem  isbasis3g 11911* 
Express the predicate "the set 𝐵 is a basis for a topology".
Definition of basis in [Munkres] p. 78.
(Contributed by NM,
17Jul2006.)

⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ (∀𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝐵∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))) 

Theorem  basis1 11912 
Property of a basis. (Contributed by NM, 16Jul2006.)

⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪
(𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷))) 

Theorem  basis2 11913* 
Property of a basis. (Contributed by NM, 17Jul2006.)

⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))) 

Theorem  fiinbas 11914* 
If a set is closed under finite intersection, then it is a basis for a
topology. (Contributed by Jeff Madsen, 2Sep2009.)

⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases) 

Theorem  baspartn 11915* 
A disjoint system of sets is a basis for a topology. (Contributed by
Stefan O'Rear, 22Feb2015.)

⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) 

Theorem  tgval 11916* 
The topology generated by a basis. See also tgval2 11918 and tgval3 11925.
(Contributed by NM, 16Jul2006.) (Revised by Mario Carneiro,
10Jan2015.)

⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)}) 

Theorem  tgvalex 11917 
The topology generated by a basis is a set. (Contributed by Jim
Kingdon, 4Mar2023.)

⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ∈ V) 

Theorem  tgval2 11918* 
Definition of a topology generated by a basis in [Munkres] p. 78. Later
we show (in tgcl 11931) that (topGen‘𝐵) is indeed a topology
(on
∪ 𝐵, see unitg 11929). See also tgval 11916 and tgval3 11925. (Contributed
by NM, 15Jul2006.) (Revised by Mario Carneiro, 10Jan2015.)

⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))}) 

Theorem  eltg 11919 
Membership in a topology generated by a basis. (Contributed by NM,
16Jul2006.) (Revised by Mario Carneiro, 10Jan2015.)

⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪
(𝐵 ∩ 𝒫 𝐴))) 

Theorem  eltg2 11920* 
Membership in a topology generated by a basis. (Contributed by NM,
15Jul2006.) (Revised by Mario Carneiro, 10Jan2015.)

⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) 

Theorem  eltg2b 11921* 
Membership in a topology generated by a basis. (Contributed by Mario
Carneiro, 17Jun2014.) (Revised by Mario Carneiro, 10Jan2015.)

⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) 

Theorem  eltg4i 11922 
An open set in a topology generated by a basis is the union of all basic
open sets contained in it. (Contributed by Stefan O'Rear,
22Feb2015.)

⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴)) 

Theorem  eltg3i 11923 
The union of a set of basic open sets is in the generated topology.
(Contributed by Mario Carneiro, 30Aug2015.)

⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵)) 

Theorem  eltg3 11924* 
Membership in a topology generated by a basis. (Contributed by NM,
15Jul2006.) (Revised by Jim Kingdon, 4Mar2023.)

⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥))) 

Theorem  tgval3 11925* 
Alternate expression for the topology generated by a basis. Lemma 2.1
of [Munkres] p. 80. See also tgval 11916 and tgval2 11918. (Contributed by
NM, 17Jul2006.) (Revised by Mario Carneiro, 30Aug2015.)

⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)}) 

Theorem  tg1 11926 
Property of a member of a topology generated by a basis. (Contributed
by NM, 20Jul2006.)

⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵) 

Theorem  tg2 11927* 
Property of a member of a topology generated by a basis. (Contributed
by NM, 20Jul2006.)

⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴)) 

Theorem  bastg 11928 
A member of a basis is a subset of the topology it generates.
(Contributed by NM, 16Jul2006.) (Revised by Mario Carneiro,
10Jan2015.)

⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵)) 

Theorem  unitg 11929 
The topology generated by a basis 𝐵 is a topology on ∪ 𝐵.
Importantly, this theorem means that we don't have to specify separately
the base set for the topological space generated by a basis. In other
words, any member of the class TopBases
completely specifies the
basis it corresponds to. (Contributed by NM, 16Jul2006.) (Proof
shortened by OpenAI, 30Mar2020.)

⊢ (𝐵 ∈ 𝑉 → ∪
(topGen‘𝐵) = ∪ 𝐵) 

Theorem  tgss 11930 
Subset relation for generated topologies. (Contributed by NM,
7May2007.)

⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶)) 

Theorem  tgcl 11931 
Show that a basis generates a topology. Remark in [Munkres] p. 79.
(Contributed by NM, 17Jul2006.)

⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top) 

Theorem  tgclb 11932 
The property tgcl 11931 can be reversed: if the topology generated
by 𝐵
is actually a topology, then 𝐵 must be a topological basis. This
yields an alternative definition of TopBases.
(Contributed by
Mario Carneiro, 2Sep2015.)

⊢ (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top) 

Theorem  tgtopon 11933 
A basis generates a topology on ∪
𝐵. (Contributed by
Mario
Carneiro, 14Aug2015.)

⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵)) 

Theorem  topbas 11934 
A topology is its own basis. (Contributed by NM, 17Jul2006.)

⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases) 

Theorem  tgtop 11935 
A topology is its own basis. (Contributed by NM, 18Jul2006.)

⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽) 

Theorem  eltop 11936 
Membership in a topology, expressed without quantifiers. (Contributed
by NM, 19Jul2006.)

⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪
(𝐽 ∩ 𝒫 𝐴))) 

Theorem  eltop2 11937* 
Membership in a topology. (Contributed by NM, 19Jul2006.)

⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) 

Theorem  eltop3 11938* 
Membership in a topology. (Contributed by NM, 19Jul2006.)

⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥))) 

Theorem  tgdom 11939 
A space has no more open sets than subsets of a basis. (Contributed by
Stefan O'Rear, 22Feb2015.) (Revised by Mario Carneiro,
9Apr2015.)

⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) ≼ 𝒫 𝐵) 

Theorem  tgiun 11940* 
The indexed union of a set of basic open sets is in the generated
topology. (Contributed by Mario Carneiro, 2Sep2015.)

⊢ ((𝐵 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ (topGen‘𝐵)) 

Theorem  tgidm 11941 
The topology generator function is idempotent. (Contributed by NM,
18Jul2006.) (Revised by Mario Carneiro, 2Sep2015.)

⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵)) 

Theorem  bastop 11942 
Two ways to express that a basis is a topology. (Contributed by NM,
18Jul2006.)

⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵)) 

Theorem  tgtop11 11943 
The topology generation function is onetoone when applied to completed
topologies. (Contributed by NM, 18Jul2006.)

⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ (topGen‘𝐽) = (topGen‘𝐾)) → 𝐽 = 𝐾) 

Theorem  en1top 11944 
{∅} is the only topology with one element.
(Contributed by FL,
18Aug2008.)

⊢ (𝐽 ∈ Top → (𝐽 ≈ 1_{o} ↔ 𝐽 = {∅})) 

Theorem  tgss3 11945 
A criterion for determining whether one topology is finer than another.
Lemma 2.2 of [Munkres] p. 80 using
abbreviations. (Contributed by NM,
20Jul2006.) (Proof shortened by Mario Carneiro, 2Sep2015.)

⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → ((topGen‘𝐵) ⊆ (topGen‘𝐶) ↔ 𝐵 ⊆ (topGen‘𝐶))) 

Theorem  tgss2 11946* 
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, 20Jul2006.) (Proof shortened by Mario Carneiro,
2Sep2015.)

⊢ ((𝐵 ∈ 𝑉 ∧ ∪ 𝐵 = ∪
𝐶) →
((topGen‘𝐵) ⊆
(topGen‘𝐶) ↔
∀𝑥 ∈ ∪ 𝐵∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝐶 (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)))) 

Theorem  basgen 11947 
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, 22Jul2006.) (Revised by Mario
Carneiro, 2Sep2015.)

⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = 𝐽) 

Theorem  basgen2 11948* 
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, 20Jul2006.) (Proof shortened by Mario Carneiro,
2Sep2015.)

⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥)) → (topGen‘𝐵) = 𝐽) 

Theorem  2basgeng 11949 
Conditions that determine the equality of two generated topologies.
(Contributed by NM, 8May2007.) (Revised by Jim Kingdon,
5Mar2023.)

⊢ ((𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ (topGen‘𝐵)) → (topGen‘𝐵) = (topGen‘𝐶)) 

Theorem  bastop1 11950* 
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,
2Feb2008.) (Proof shortened by Mario Carneiro, 2Sep2015.)

⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽) → ((topGen‘𝐵) = 𝐽 ↔ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))) 

Theorem  bastop2 11951* 
A version of bastop1 11950 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent.
(Contributed by NM, 3Feb2008.)

⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)))) 

6.1.3 Examples of topologies


Theorem  distop 11952 
The discrete topology on a set 𝐴. Part of Example 2 in [Munkres]
p. 77. (Contributed by FL, 17Jul2006.) (Revised by Mario Carneiro,
19Mar2015.)

⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) 

Theorem  topnex 11953 
The class of all topologies is a proper class. The proof uses
discrete topologies and pwnex 4299. (Contributed by BJ, 2May2021.)

⊢ Top ∉ V 

Theorem  distopon 11954 
The discrete topology on a set 𝐴, with base set. (Contributed by
Mario Carneiro, 13Aug2015.)

⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴)) 

Theorem  sn0topon 11955 
The singleton of the empty set is a topology on the empty set.
(Contributed by Mario Carneiro, 13Aug2015.)

⊢ {∅} ∈
(TopOn‘∅) 

Theorem  sn0top 11956 
The singleton of the empty set is a topology. (Contributed by Stefan
Allan, 3Mar2006.) (Proof shortened by Mario Carneiro,
13Aug2015.)

⊢ {∅} ∈ Top 

Theorem  epttop 11957* 
The excluded point topology. (Contributed by Mario Carneiro,
3Sep2015.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴)) 

Theorem  distps 11958 
The discrete topology on a set 𝐴 expressed as a topological space.
(Contributed by FL, 20Aug2006.)

⊢ 𝐴 ∈ V & ⊢ 𝐾 = {⟨(Base‘ndx),
𝐴⟩,
⟨(TopSet‘ndx), 𝒫 𝐴⟩} ⇒ ⊢ 𝐾 ∈ TopSp 

6.1.4 Closure and interior


Syntax  ccld 11959 
Extend class notation with the set of closed sets of a topology.

class Clsd 

Syntax  cnt 11960 
Extend class notation with interior of a subset of a topology base set.

class int 

Syntax  ccl 11961 
Extend class notation with closure of a subset of a topology base set.

class cls 

Definition  dfcld 11962* 
Define a function on topologies whose value is the set of closed sets of
the topology. (Contributed by NM, 2Oct2006.)

⊢ Clsd = (𝑗 ∈ Top ↦ {𝑥 ∈ 𝒫 ∪ 𝑗
∣ (∪ 𝑗 ∖ 𝑥) ∈ 𝑗}) 

Definition  dfntr 11963* 
Define a function on topologies whose value is the interior function on
the subsets of the base set. See ntrval 11977. (Contributed by NM,
10Sep2006.)

⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∪ (𝑗 ∩ 𝒫 𝑥))) 

Definition  dfcls 11964* 
Define a function on topologies whose value is the closure function on
the subsets of the base set. See clsval 11978. (Contributed by NM,
3Oct2006.)

⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗
↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦})) 

Theorem  fncld 11965 
The closedset generator is a wellbehaved function. (Contributed by
Stefan O'Rear, 1Feb2015.)

⊢ Clsd Fn Top 

Theorem  cldval 11966* 
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, 2Oct2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ 𝐽}) 

Theorem  ntrfval 11967* 
The interior function on the subsets of a topology's base set.
(Contributed by NM, 10Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (int‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∪
(𝐽 ∩ 𝒫 𝑥))) 

Theorem  clsfval 11968* 
The closure function on the subsets of a topology's base set.
(Contributed by NM, 3Oct2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (cls‘𝐽) = (𝑥 ∈ 𝒫 𝑋 ↦ ∩
{𝑦 ∈
(Clsd‘𝐽) ∣
𝑥 ⊆ 𝑦})) 

Theorem  cldrcl 11969 
Reverse closure of the closed set operation. (Contributed by Stefan
O'Rear, 22Feb2015.)

⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) 

Theorem  iscld 11970 
The predicate "the class 𝑆 is a closed set". (Contributed
by NM,
2Oct2006.) (Revised by Mario Carneiro, 11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑆 ⊆ 𝑋 ∧ (𝑋 ∖ 𝑆) ∈ 𝐽))) 

Theorem  iscld2 11971 
A subset of the underlying set of a topology is closed iff its
complement is open. (Contributed by NM, 4Oct2006.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑆) ∈ 𝐽)) 

Theorem  cldss 11972 
A closed set is a subset of the underlying set of a topology.
(Contributed by NM, 5Oct2006.) (Revised by Stefan O'Rear,
22Feb2015.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ 𝑋) 

Theorem  cldss2 11973 
The set of closed sets is contained in the powerset of the base.
(Contributed by Mario Carneiro, 6Jan2014.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋 

Theorem  cldopn 11974 
The complement of a closed set is open. (Contributed by NM,
5Oct2006.) (Revised by Stefan O'Rear, 22Feb2015.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝑆 ∈ (Clsd‘𝐽) → (𝑋 ∖ 𝑆) ∈ 𝐽) 

Theorem  difopn 11975 
The difference of a closed set with an open set is open. (Contributed
by Mario Carneiro, 6Jan2014.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽) 

Theorem  topcld 11976 
The underlying set of a topology is closed. Part of Theorem 6.1(1) of
[Munkres] p. 93. (Contributed by NM,
3Oct2006.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽)) 

Theorem  ntrval 11977 
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, 10Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = ∪ (𝐽 ∩ 𝒫 𝑆)) 

Theorem  clsval 11978* 
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, 10Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = ∩ {𝑥 ∈ (Clsd‘𝐽) ∣ 𝑆 ⊆ 𝑥}) 

Theorem  0cld 11979 
The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93.
(Contributed by NM, 4Oct2006.)

⊢ (𝐽 ∈ Top → ∅ ∈
(Clsd‘𝐽)) 

Theorem  uncld 11980 
The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of
[Munkres] p. 93. (Contributed by NM,
5Oct2006.)

⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∪ 𝐵) ∈ (Clsd‘𝐽)) 

Theorem  cldcls 11981 
A closed subset equals its own closure. (Contributed by NM,
15Mar2007.)

⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆) 

Theorem  iuncld 11982* 
A finite indexed union of closed sets is closed. (Contributed by Mario
Carneiro, 19Sep2015.) (Revised by Jim Kingdon, 10Mar2023.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) 

Theorem  unicld 11983 
A finite union of closed sets is closed. (Contributed by Mario
Carneiro, 19Sep2015.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪
𝐴 ∈ (Clsd‘𝐽)) 

Theorem  ntropn 11984 
The interior of a subset of a topology's underlying set is open.
(Contributed by NM, 11Sep2006.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ∈ 𝐽) 

Theorem  clsss 11985 
Subset relationship for closure. (Contributed by NM, 10Feb2007.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆)) 

Theorem  ntrss 11986 
Subset relationship for interior. (Contributed by NM, 3Oct2007.)
(Revised by Jim Kingdon, 11Mar2023.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆)) 

Theorem  sscls 11987 
A subset of a topology's underlying set is included in its closure.
(Contributed by NM, 22Feb2007.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) 

Theorem  ntrss2 11988 
A subset includes its interior. (Contributed by NM, 3Oct2007.)
(Revised by Mario Carneiro, 11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆) 

Theorem  ssntr 11989 
An open subset of a set is a subset of the set's interior. (Contributed
by Jeff Hankins, 31Aug2009.) (Revised by Mario Carneiro,
11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) ∧ (𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ 𝑆)) → 𝑂 ⊆ ((int‘𝐽)‘𝑆)) 

Theorem  ntrss3 11990 
The interior of a subset of a topological space is included in the
space. (Contributed by NM, 1Oct2007.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋) 

Theorem  ntrin 11991 
A pairwise intersection of interiors is the interior of the
intersection. This does not always hold for arbitrary intersections.
(Contributed by Jeff Hankins, 31Aug2009.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((int‘𝐽)‘(𝐴 ∩ 𝐵)) = (((int‘𝐽)‘𝐴) ∩ ((int‘𝐽)‘𝐵))) 

Theorem  isopn3 11992 
A subset is open iff it equals its own interior. (Contributed by NM,
9Oct2006.) (Revised by Mario Carneiro, 11Nov2013.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ 𝐽 ↔ ((int‘𝐽)‘𝑆) = 𝑆)) 

Theorem  ntridm 11993 
The interior operation is idempotent. (Contributed by NM,
2Oct2007.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆)) 

Theorem  clstop 11994 
The closure of a topology's underlying set is the entire set.
(Contributed by NM, 5Oct2007.) (Proof shortened by Jim Kingdon,
11Mar2023.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘𝑋) = 𝑋) 

Theorem  ntrtop 11995 
The interior of a topology's underlying set is the entire set.
(Contributed by NM, 12Sep2006.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → ((int‘𝐽)‘𝑋) = 𝑋) 

Theorem  clsss2 11996 
If a subset is included in a closed set, so is the subset's closure.
(Contributed by NM, 22Feb2007.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐶 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝐶) → ((cls‘𝐽)‘𝑆) ⊆ 𝐶) 

Theorem  clsss3 11997 
The closure of a subset of a topological space is included in the space.
(Contributed by NM, 26Feb2007.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋) 

Theorem  ntrcls0 11998 
A subset whose closure has an empty interior also has an empty interior.
(Contributed by NM, 4Oct2007.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ((int‘𝐽)‘((cls‘𝐽)‘𝑆)) = ∅) → ((int‘𝐽)‘𝑆) = ∅) 

Theorem  ntreq0 11999* 
Two ways to say that a subset has an empty interior. (Contributed by
NM, 3Oct2007.) (Revised by Jim Kingdon, 11Mar2023.)

⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (((int‘𝐽)‘𝑆) = ∅ ↔ ∀𝑥 ∈ 𝐽 (𝑥 ⊆ 𝑆 → 𝑥 = ∅))) 

Theorem  cls0 12000 
The closure of the empty set. (Contributed by NM, 2Oct2007.) (Proof
shortened by Jim Kingdon, 12Mar2023.)

⊢ (𝐽 ∈ Top → ((cls‘𝐽)‘∅) =
∅) 