P. 233 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23201-23300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tgclb 23201	The property tgcl 23200 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 23202	A basis generates a topology on ∪ 𝐵. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (𝐵 ∈ TopBases → (topGen‘𝐵) ∈ (TopOn‘∪ 𝐵))
Theorem	topbas 23203	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
⊢ (𝐽 ∈ Top → 𝐽 ∈ TopBases)
Theorem	tgtop 23204	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐽 ∈ Top → (topGen‘𝐽) = 𝐽)
Theorem	eltop 23205	Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ 𝐴 ⊆ ∪ (𝐽 ∩ 𝒫 𝐴)))
Theorem	eltop2 23206*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))
Theorem	eltop3 23207*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
⊢ (𝐽 ∈ Top → (𝐴 ∈ 𝐽 ↔ ∃𝑥(𝑥 ⊆ 𝐽 ∧ 𝐴 = ∪ 𝑥)))
Theorem	fibas 23208	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 23209	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 23210*	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 23211	The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
⊢ (𝐵 ∈ 𝑉 → (topGen‘(topGen‘𝐵)) = (topGen‘𝐵))
Theorem	bastop 23212	Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ Top ↔ (topGen‘𝐵) = 𝐵))
Theorem	tgtop11 23213	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 23214	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 23215	{∅} is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
⊢ (𝐽 ∈ Top → (𝐽 ≈ 1o ↔ 𝐽 = {∅}))
Theorem	en2top 23216	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 23217	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 23218*	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 23219	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 23220*	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 23221	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 23222	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 23223	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 23224*	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 23225*	A version of bastop1 23224 that doesn't have 𝐵 ⊆ 𝐽 in the antecedent. (Contributed by NM, 3-Feb-2008.)
⊢ (𝐽 ∈ Top → ((topGen‘𝐵) = 𝐽 ↔ (𝐵 ⊆ 𝐽 ∧ ∀𝑥 ∈ 𝐽 ∃𝑦(𝑦 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑦))))
12.1.3  Examples of topologies
Theorem	distop 23226	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 23227	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 7762; an alternate proof uses indiscrete topologies (see indistop 23233) and the analogue of pwnex 7762 with pairs {∅, 𝑥} instead of power sets 𝒫 𝑥 (that analogue is also a consequence of abnex 7760). (Contributed by BJ, 2-May-2021.)
⊢ Top ∉ V
Theorem	distopon 23228	The discrete topology on a set 𝐴, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ (TopOn‘𝐴))
Theorem	sn0topon 23229	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ {∅} ∈ (TopOn‘∅)
Theorem	sn0top 23230	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 23231	A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ {∅, ( I ‘𝐴)} = {∅, 𝐴}
Theorem	indistopon 23232	The indiscrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → {∅, 𝐴} ∈ (TopOn‘𝐴))
Theorem	indistop 23233	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 23234	The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ( I ‘𝐴) = ∪ {∅, 𝐴}
Theorem	fctop 23235*	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 23236*	The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (This version of fctop 23235 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.)
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ≺ ω ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	cctop 23237*	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 23238*	The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Theorem	pptbas 23239*	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 23240*	The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃 ∈ 𝑥 → 𝑥 = 𝐴)} ∈ (TopOn‘𝐴))
Theorem	indistpsx 23241	The indiscrete topology on a set 𝐴 expressed as a topological space, using explicit structure component references. Compare with indistps 23242 and indistps2 23243. The advantage of this version is that the actual function for the structure is evident, and df-ndx 17292 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 17308 and df-tset 17367 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 23242 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐾 = {⟨1, 𝐴⟩, ⟨9, {∅, 𝐴}⟩}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistps 23242	The indiscrete topology on a set 𝐴 expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 23241 is that it is independent of the indices of the component definitions df-base 17308 and df-tset 17367, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 23243 is that it is easy to eliminate the hypotheses with eqid 2762 and vtoclg 3520 to result in a closed theorem. Theorems indistpsALT 23244 and indistps2ALT 23245 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 23243	The indiscrete topology on a set 𝐴 expressed as a topological space, using direct component assignments. Compare with indistps 23242. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 23244 and indistps2ALT 23245 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	indistpsALT 23244	The indiscrete topology on a set 𝐴 expressed as a topological space. Here we show how to derive the structural version indistps 23242 from the direct component assignment version indistps2 23243. (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 23245	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 23243 from the structural version indistps 23242. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (Base‘𝐾) = 𝐴    &   ⊢ (TopOpen‘𝐾) = {∅, 𝐴}    ⇒   ⊢ 𝐾 ∈ TopSp
Theorem	distps 23246	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 23247	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 23248	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 23249	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 23250*	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 23251*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 23267. (Contributed by NM, 10-Sep-2006.)
⊢ int = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∪ (𝑗 ∩ 𝒫 𝑥)))
Definition	df-cls 23252*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 23268. (Contributed by NM, 3-Oct-2006.)
⊢ cls = (𝑗 ∈ Top ↦ (𝑥 ∈ 𝒫 ∪ 𝑗 ↦ ∩ {𝑦 ∈ (Clsd‘𝑗) ∣ 𝑥 ⊆ 𝑦}))
Theorem	fncld 23253	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
⊢ Clsd Fn Top
Theorem	cldval 23254*	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 23255*	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 23256*	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 23257	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top)
Theorem	iscld 23258	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 23259	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 23260	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 23261	The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ (Clsd‘𝐽) ⊆ 𝒫 𝑋
Theorem	cldopn 23262	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 23263	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 23264	The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ∈ 𝐽) → (𝑋 ∖ 𝑆) ∈ (Clsd‘𝐽))
Theorem	difopn 23265	The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ (Clsd‘𝐽)) → (𝐴 ∖ 𝐵) ∈ 𝐽)
Theorem	topcld 23266	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 23267	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 23268*	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 23269	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 23270*	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 23271	The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.)
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∩ 𝐴 ∈ (Clsd‘𝐽))
Theorem	uncld 23272	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 23273	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
⊢ (𝑆 ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘𝑆) = 𝑆)
Theorem	incld 23274	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 23275*	An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ (Clsd‘𝐽))
Theorem	iuncld 23276*	A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽)) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ (Clsd‘𝐽))
Theorem	unicld 23277	A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ 𝐴 ⊆ (Clsd‘𝐽)) → ∪ 𝐴 ∈ (Clsd‘𝐽))
Theorem	clscld 23278	The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽))
Theorem	clsf 23279	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 23280	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 23281	Express closure in terms of interior. (Contributed by NM, 10-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑋 ∖ ((int‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrval2 23282	Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) = (𝑋 ∖ ((cls‘𝐽)‘(𝑋 ∖ 𝑆))))
Theorem	ntrdif 23283	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 23284	A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → ((cls‘𝐽)‘(𝑋 ∖ 𝐴)) = (𝑋 ∖ ((int‘𝐽)‘𝐴)))
Theorem	clsss 23285	Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((cls‘𝐽)‘𝑇) ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss 23286	Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑇 ⊆ 𝑆) → ((int‘𝐽)‘𝑇) ⊆ ((int‘𝐽)‘𝑆))
Theorem	sscls 23287	A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆))
Theorem	ntrss2 23288	A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑆)
Theorem	ssntr 23289	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 23290	The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrss3 23291	The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘𝑆) ⊆ 𝑋)
Theorem	ntrin 23292	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 23293	The complement of a closure is open. (Contributed by NM, 11-Sep-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑋 ∖ ((cls‘𝐽)‘𝑆)) ∈ 𝐽)
Theorem	cmntrcld 23294	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 23295	A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) = 𝑆))
Theorem	iscld4 23296	A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((cls‘𝐽)‘𝑆) ⊆ 𝑆))
Theorem	isopn3 23297	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 23298	The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((cls‘𝐽)‘𝑆))
Theorem	ntridm 23299	The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
⊢ 𝑋 = ∪ 𝐽    ⇒   ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((int‘𝐽)‘((int‘𝐽)‘𝑆)) = ((int‘𝐽)‘𝑆))
Theorem	clstop 23300	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‘𝐽)‘𝑋) = 𝑋)