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	toponcomb 23101	Biconditional form of toponcom 23100. (Contributed by BJ, 5-Dec-2021.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘∪ 𝐾) ↔ 𝐾 ∈ (TopOn‘∪ 𝐽)))
Theorem	topgele 23102	The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋))
Theorem	topsn 23103	The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4868). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ (𝐽 ∈ (TopOn‘{𝐴}) → 𝐽 = 𝒫 {𝐴})
12.1.1.3  Topological spaces
Syntax	ctps 23104	Syntax for the class of topological spaces.
class TopSp
Definition	df-topsp 23105	Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
Theorem	istps 23106	Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))
Theorem	istps2 23107	Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽))
Theorem	tpsuni 23108	The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽)
Theorem	tpstop 23109	The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top)
Theorem	tpspropd 23110	A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp))
Theorem	tpsprop2d 23111	A topological space depends only on the base and topology components. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp))
Theorem	topontopn 23112	Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopSet‘𝐾)    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾))
Theorem	tsettps 23113	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, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopSet‘𝐾)    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp)
Theorem	istpsi 23114	Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = 𝐽    &   ⊢ 𝐴 = ∪ 𝐽    &   ⊢ 𝐽 ∈ Top    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	eltpsg 23115	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by AV, 31-Oct-2024.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝐽⟩}    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp)
Theorem	eltpsi 23116	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by NM, 20-Oct-2012.) (Revised by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐾 = {⟨(Base‘ndx), 𝐴⟩, ⟨(TopSet‘ndx), 𝐽⟩}    &   ⊢ 𝐴 = ∪ 𝐽    &   ⊢ 𝐽 ∈ Top    ⇒   ⊢ 𝐾 ∈ TopSp
12.1.2  Topological bases
Syntax	ctb 23117	Syntax for the class of topological bases.
class TopBases
Definition	df-bases 23118*	Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 23120). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}
Theorem	isbasisg 23119*	Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))))
Theorem	isbasis2g 23120*	Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))
Theorem	isbasis3g 23121*	Express the predicate "the set 𝐵 is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ (∀𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝐵∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))))
Theorem	basis1 23122	Property of a basis. (Contributed by NM, 16-Jul-2006.)
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷)))
Theorem	basis2 23123*	Property of a basis. (Contributed by NM, 17-Jul-2006.)
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))
Theorem	fiinbas 23124*	If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases)
Theorem	basdif0 23125	A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015.)
⊢ ((𝐵 ∖ {∅}) ∈ TopBases ↔ 𝐵 ∈ TopBases)
Theorem	baspartn 23126*	A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases)
Theorem	tgval 23127*	The topology generated by a basis. See also tgval2 23128 and tgval3 23135. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)})
Theorem	tgval2 23128*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 23141) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵, see unitg 23139). See also tgval 23127 and tgval3 23135. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))})
Theorem	eltg 23129	Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴)))
Theorem	eltg2 23130*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))))
Theorem	eltg2b 23131*	Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
Theorem	eltg4i 23132	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, 22-Feb-2015.)
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴))
Theorem	eltg3i 23133	The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵))
Theorem	eltg3 23134*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥)))
Theorem	tgval3 23135*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 23127 and tgval2 23128. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)})
Theorem	tg1 23136	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵)
Theorem	tg2 23137*	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))
Theorem	bastg 23138	A member of a basis is a subset of the topology it generates. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (topGen‘𝐵))
Theorem	unitg 23139	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, 16-Jul-2006.) (Proof shortened by OpenAI, 30-Mar-2020.)
⊢ (𝐵 ∈ 𝑉 → ∪ (topGen‘𝐵) = ∪ 𝐵)
Theorem	tgss 23140	Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶))
Theorem	tgcl 23141	Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
Theorem	tgclb 23142	The property tgcl 23141 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, 2-Sep-2015.)
⊢ (𝐵 ∈ TopBases ↔ (topGen‘𝐵) ∈ Top)
Theorem	tgtopon 23143	A basis generates a topology on ∪ 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵))
Theorem	topbas 23144	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases)
Theorem	tgtop 23145	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)
Theorem	eltop 23146	Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ (𝐽 ∩ 𝒫 𝐴)))
Theorem	eltop2 23147*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
Theorem	eltop3 23148*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥)))
Theorem	fibas 23149	A collection of finite intersections is a basis. The initial set is a subbasis for the topology. (Contributed by Jeff Hankins, 25-Aug-2009.) (Revised by Mario Carneiro, 24-Nov-2013.)
⊢ (fi‘𝐴) ∈ TopBases
Theorem	tgdom 23150	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 23151*	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 23152	The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))
Theorem	bastop 23153	Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))
Theorem	tgtop11 23154	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 23155	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 23156	{∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅}))
Theorem	en2top 23157	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 23158	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 23159*	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 23160	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 23161*	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 23162	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 23163	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 23164	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 23165*	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 23166*	A version of bastop1 23165 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.)
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))))
12.1.3  Examples of topologies
Theorem	distop 23167	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 23168	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7760; an alternate proof uses indiscrete topologies (see indistop 23174) and the analogue of pwnex 7760 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7758). (Contributed by BJ, 2-May-2021.)
⊢ Top ∉ V
Theorem	distopon 23169	The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
Theorem	sn0topon 23170	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ {∅} ∈ (TopOn‘∅)
Theorem	sn0top 23171	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 23172	A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴}
Theorem	indistopon 23173	The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴))
Theorem	indistop 23174	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 23175	The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴}
Theorem	fctop 23176*	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 23177*	The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 23176 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	cctop 23178*	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 23179*	The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	pptbas 23180*	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 23181*	The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
Theorem	indistpsx 23182	The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 23183 and indistps2 23184. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17264 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 17280 and df-tset 17339 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 23183 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨1, 𝐴⟩, ⟨9, {∅, 𝐴}⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistps 23183	The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 23182 is that it is independent of the indices of the component definitions df-base 17280 and df-tset 17339, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 23184 is that it is easy to eliminate the hypotheses with eqid 2766 and vtoclg 3525 to result in a closed theorem. Theorems indistpsALT 23185 and indistps2ALT 23186 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 23184	The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 23183. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 23185 and indistps2ALT 23186 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistpsALT 23185	The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 23183 from the direct component assignment version indistps2 23184. (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 23186	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 23184 from the structural version indistps 23183. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	distps 23187	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 23188	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 23189	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 23190	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 23191*	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 23192*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 23208. (Contributed by NM, 10-Sep-2006.)
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
Definition	df-cls 23193*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 23209. (Contributed by NM, 3-Oct-2006.)
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))
Theorem	fncld 23194	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ Clsd Fn Top
Theorem	cldval 23195*	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 23196*	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 23197*	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 23198	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
Theorem	iscld 23199	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 23200	A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑆) ∈ 𝐽))