P. 229 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 22801-22900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	toponuni 22801	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
Theorem	topontopi 22802	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐽 ∈ Top
Theorem	toponunii 22803	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐽 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐵 = ∪ 𝐽
Theorem	toptopon 22804	Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
Theorem	toptopon2 22805	A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
Theorem	topontopon 22806	A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ (TopOn‘∪ 𝐽))
Theorem	funtopon 22807	The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.)
⊢ Fun TopOn
Theorem	toponrestid 22808	Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.)
⊢ 𝐴 ∈ (TopOn‘𝐵)    ⇒   ⊢ 𝐴 = (𝐴 ↾t 𝐵)
Theorem	toponsspwpw 22809	The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.)
⊢ (TopOn‘𝐴) ⊆ 𝒫 𝒫 𝐴
Theorem	dmtopon 22810	The domain of TopOn is the universal class V. (Contributed by BJ, 29-Apr-2021.)
⊢ dom TopOn = V
Theorem	fntopon 22811	The class TopOn is a function with domain the universal class V. Analogue for topologies of fnmre 17552 for Moore collections. (Contributed by BJ, 29-Apr-2021.)
⊢ TopOn Fn V
Theorem	toprntopon 22812	A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021.)
⊢ Top = ∪ ran TopOn
Theorem	toponmax 22813	The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽)
Theorem	toponss 22814	A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋)
Theorem	toponcom 22815	If 𝐾 is a topology on the base set of topology 𝐽, then 𝐽 is a topology on the base of 𝐾. (Contributed by Mario Carneiro, 22-Aug-2015.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ (TopOn‘∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐾))
Theorem	toponcomb 22816	Biconditional form of toponcom 22815. (Contributed by BJ, 5-Dec-2021.)
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘∪ 𝐾) ↔ 𝐾 ∈ (TopOn‘∪ 𝐽)))
Theorem	topgele 22817	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 22818	The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4864). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
⊢ (𝐽 ∈ (TopOn‘{𝐴}) → 𝐽 = 𝒫 {𝐴})
12.1.1.3  Topological spaces
Syntax	ctps 22819	Syntax for the class of topological spaces.
class TopSp
Definition	df-topsp 22820	Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))}
Theorem	istps 22821	Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴))
Theorem	istps2 22822	Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽))
Theorem	tpsuni 22823	The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽)
Theorem	tpstop 22824	The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
⊢ 𝐽 = (TopOpen‘𝐾)    ⇒   ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top)
Theorem	tpspropd 22825	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 22826	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 22827	Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ 𝐴 = (Base‘𝐾)    &   ⊢ 𝐽 = (TopSet‘𝐾)    ⇒   ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾))
Theorem	tsettps 22828	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 22829	Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = 𝐽    &   ⊢ 𝐴 = ∪ 𝐽    &   ⊢ 𝐽 ∈ Top    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	eltpsg 22830	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 22831	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 22832	Syntax for the class of topological bases.
class TopBases
Definition	df-bases 22833*	Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 22835). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}
Theorem	isbasisg 22834*	Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦))))
Theorem	isbasis2g 22835*	Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))
Theorem	isbasis3g 22836*	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 22837	Property of a basis. (Contributed by NM, 16-Jul-2006.)
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷)))
Theorem	basis2 22838*	Property of a basis. (Contributed by NM, 17-Jul-2006.)
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))
Theorem	fiinbas 22839*	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 22840	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 22841*	A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases)
Theorem	tgval 22842*	The topology generated by a basis. See also tgval2 22843 and tgval3 22850. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)})
Theorem	tgval2 22843*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 22856) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵, see unitg 22854). See also tgval 22842 and tgval3 22850. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))})
Theorem	eltg 22844	Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴)))
Theorem	eltg2 22845*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))))
Theorem	eltg2b 22846*	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 22847	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 22848	The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵))
Theorem	eltg3 22849*	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 22850*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 22842 and tgval2 22843. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦)})
Theorem	tg1 22851	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 ⊆ ∪ 𝐵)
Theorem	tg2 22852*	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
⊢ ((𝐴 ∈ (topGen‘𝐵) ∧ 𝐶 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 (𝐶 ∈ 𝑥 ∧ 𝑥 ⊆ 𝐴))
Theorem	bastg 22853	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 22854	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 22855	Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶) → (topGen‘𝐵) ⊆ (topGen‘𝐶))
Theorem	tgcl 22856	Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ Top)
Theorem	tgclb 22857	The property tgcl 22856 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 22858	A basis generates a topology on ∪ 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵))
Theorem	topbas 22859	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases)
Theorem	tgtop 22860	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)
Theorem	eltop 22861	Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ (𝐽 ∩ 𝒫 𝐴)))
Theorem	eltop2 22862*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
Theorem	eltop3 22863*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥)))
Theorem	fibas 22864	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 22865	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 22866*	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 22867	The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))
Theorem	bastop 22868	Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))
Theorem	tgtop11 22869	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 22870	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 22871	{∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅}))
Theorem	en2top 22872	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 22873	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 22874*	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 22875	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 22876*	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 22877	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 22878	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 22879	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 22880*	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 22881*	A version of bastop1 22880 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.)
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))))
12.1.3  Examples of topologies
Theorem	distop 22882	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 22883	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7735; an alternate proof uses indiscrete topologies (see indistop 22889) and the analogue of pwnex 7735 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7733). (Contributed by BJ, 2-May-2021.)
⊢ Top ∉ V
Theorem	distopon 22884	The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
Theorem	sn0topon 22885	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ {∅} ∈ (TopOn‘∅)
Theorem	sn0top 22886	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 22887	A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴}
Theorem	indistopon 22888	The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴))
Theorem	indistop 22889	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 22890	The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴}
Theorem	fctop 22891*	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 22892*	The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 22891 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	cctop 22893*	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 22894*	The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	pptbas 22895*	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 22896*	The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
Theorem	indistpsx 22897	The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 22898 and indistps2 22899. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17164 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 17180 and df-tset 17239 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 22898 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨1, 𝐴⟩, ⟨9, {∅, 𝐴}⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistps 22898	The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 22897 is that it is independent of the indices of the component definitions df-base 17180 and df-tset 17239, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 22899 is that it is easy to eliminate the hypotheses with eqid 2729 and vtoclg 3520 to result in a closed theorem. Theorems indistpsALT 22900 and indistps2ALT 22901 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 22899	The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 22898. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 22900 and indistps2ALT 22901 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistpsALT 22900	The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 22898 from the direct component assignment version indistps2 22899. (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