P. 137 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13601-13700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	topontopi 13601	A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- J e. (TopOn ` B )   =>    |- J e. Top
Theorem	toponunii 13602	The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- J e. (TopOn ` B )   =>    |- B = U. J
Theorem	toptopon 13603	Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( J e. Top <-> J e. (TopOn ` X ) )
Theorem	toptopon2 13604	A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
|- ( J e. Top <-> J e. (TopOn ` U. J ) )
Theorem	topontopon 13605	A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)
|- ( J e. (TopOn ` X ) -> J e. (TopOn ` U. J ) )
Theorem	toponrestid 13606	Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.)
|- A e. (TopOn ` B )   =>    |- A = ( A ↾t B )
Theorem	toponsspwpwg 13607	The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon, 16-Jan-2023.)
|- ( A e. V -> (TopOn ` A ) C_ ~P ~P A )
Theorem	dmtopon 13608	The domain of TopOn is _V. (Contributed by BJ, 29-Apr-2021.)
|- dom TopOn = _V
Theorem	fntopon 13609	The class TopOn is a function with domain _V. (Contributed by BJ, 29-Apr-2021.)
|- TopOn Fn _V
Theorem	toponmax 13610	The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( J e. (TopOn ` B ) -> B e. J )
Theorem	toponss 13611	A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. J ) -> A C_ X )
Theorem	toponcom 13612	If K is a topology on the base set of topology J, then J is a topology on the base of K. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( ( J e. Top /\ K e. (TopOn ` U. J ) ) -> J e. (TopOn ` U. K ) )
Theorem	toponcomb 13613	Biconditional form of toponcom 13612. (Contributed by BJ, 5-Dec-2021.)
|- ( ( J e. Top /\ K e. Top ) -> ( J e. (TopOn ` U. K ) <-> K e. (TopOn ` U. J ) ) )
Theorem	topgele 13614	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.)
|- ( J e. (TopOn ` X ) -> ( { (/) , X } C_ J /\ J C_ ~P X ) )
8.1.1.3  Topological spaces
Syntax	ctps 13615	Syntax for the class of topological spaces.
class TopSp
Definition	df-topsp 13616	Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.)
|- TopSp = { f | ( TopOpen ` f ) e. (TopOn ` ( Base ` f ) ) }
Theorem	istps 13617	Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.)
|- A = ( Base ` K )   &    |- J = ( TopOpen ` K )   =>    |- ( K e. TopSp <-> J e. (TopOn ` A ) )
Theorem	istps2 13618	Express the predicate "is a topological space". (Contributed by NM, 20-Oct-2012.)
|- A = ( Base ` K )   &    |- J = ( TopOpen ` K )   =>    |- ( K e. TopSp <-> ( J e. Top /\ A = U. J ) )
Theorem	tpsuni 13619	The base set of a topological space. (Contributed by FL, 27-Jun-2014.)
|- A = ( Base ` K )   &    |- J = ( TopOpen ` K )   =>    |- ( K e. TopSp -> A = U. J )
Theorem	tpstop 13620	The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.)
|- J = ( TopOpen ` K )   =>    |- ( K e. TopSp -> J e. Top )
Theorem	tpspropd 13621	A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( ph -> ( Base ` K ) = ( Base ` L ) )   &    |- ( ph -> ( TopOpen ` K ) = ( TopOpen ` L ) )   =>    |- ( ph -> ( K e. TopSp <-> L e. TopSp ) )
Theorem	topontopn 13622	Express the predicate "is a topological space". (Contributed by Mario Carneiro, 13-Aug-2015.)
|- A = ( Base ` K )   &    |- J = (TopSet ` K )   =>    |- ( J e. (TopOn ` A ) -> J = ( TopOpen ` K ) )
Theorem	tsettps 13623	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.)
|- A = ( Base ` K )   &    |- J = (TopSet ` K )   =>    |- ( J e. (TopOn ` A ) -> K e. TopSp )
Theorem	istpsi 13624	Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.)
|- ( Base ` K ) = A   &    |- ( TopOpen ` K ) = J   &    |- A = U. J   &    |- J e. Top   =>    |- K e. TopSp
Theorem	eltpsg 13625	Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.)
|- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , J >. }   =>    |- ( J e. (TopOn ` A ) -> K e. TopSp )
Theorem	eltpsi 13626	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.)
|- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , J >. }   &    |- A = U. J   &    |- J e. Top   =>    |- K e. TopSp
8.1.2  Topological bases
Syntax	ctb 13627	Syntax for the class of topological bases.
class TopBases
Definition	df-bases 13628*	Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 13630). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.)
|- TopBases = { x | A. y e. x A. z e. x ( y i^i z ) C_ U. ( x i^i ~P ( y i^i z ) ) }
Theorem	isbasisg 13629*	Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
|- ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) )
Theorem	isbasis2g 13630*	Express the predicate "the set B is a basis for a topology". (Contributed by NM, 17-Jul-2006.)
|- ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) )
Theorem	isbasis3g 13631*	Express the predicate "the set B is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.)
|- ( B e. C -> ( B e. TopBases <-> ( A. x e. B x C_ U. B /\ A. x e. U. B E. y e. B x e. y /\ A. x e. B A. y e. B A. z e. ( x i^i y ) E. w e. B ( z e. w /\ w C_ ( x i^i y ) ) ) ) )
Theorem	basis1 13632	Property of a basis. (Contributed by NM, 16-Jul-2006.)
|- ( ( B e. TopBases /\ C e. B /\ D e. B ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) )
Theorem	basis2 13633*	Property of a basis. (Contributed by NM, 17-Jul-2006.)
|- ( ( ( B e. TopBases /\ C e. B ) /\ ( D e. B /\ A e. ( C i^i D ) ) ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) )
Theorem	fiinbas 13634*	If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( B e. C /\ A. x e. B A. y e. B ( x i^i y ) e. B ) -> B e. TopBases )
Theorem	baspartn 13635*	A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( P e. V /\ A. x e. P A. y e. P ( x = y \/ ( x i^i y ) = (/) ) ) -> P e. TopBases )
Theorem	tgval2 13636*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 13649) that ( topGen ` B ) is indeed a topology (on U. B, see unitg 13647). See also tgval 12716 and tgval3 13643. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( topGen ` B ) = { x | ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) } )
Theorem	eltg 13637	Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )
Theorem	eltg2 13638*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) )
Theorem	eltg2b 13639*	Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) )
Theorem	eltg4i 13640	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.)
|- ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) )
Theorem	eltg3i 13641	The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.)
|- ( ( B e. V /\ A C_ B ) -> U. A e. ( topGen ` B ) )
Theorem	eltg3 13642*	Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.)
|- ( B e. V -> ( A e. ( topGen ` B ) <-> E. x ( x C_ B /\ A = U. x ) ) )
Theorem	tgval3 13643*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 12716 and tgval2 13636. (Contributed by NM, 17-Jul-2006.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- ( B e. V -> ( topGen ` B ) = { x | E. y ( y C_ B /\ x = U. y ) } )
Theorem	tg1 13644	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
|- ( A e. ( topGen ` B ) -> A C_ U. B )
Theorem	tg2 13645*	Property of a member of a topology generated by a basis. (Contributed by NM, 20-Jul-2006.)
|- ( ( A e. ( topGen ` B ) /\ C e. A ) -> E. x e. B ( C e. x /\ x C_ A ) )
Theorem	bastg 13646	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.)
|- ( B e. V -> B C_ ( topGen ` B ) )
Theorem	unitg 13647	The topology generated by a basis B is a topology on U. B. 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.)
|- ( B e. V -> U. ( topGen ` B ) = U. B )
Theorem	tgss 13648	Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
|- ( ( C e. V /\ B C_ C ) -> ( topGen ` B ) C_ ( topGen ` C ) )
Theorem	tgcl 13649	Show that a basis generates a topology. Remark in [Munkres] p. 79. (Contributed by NM, 17-Jul-2006.)
|- ( B e. TopBases -> ( topGen ` B ) e. Top )
Theorem	tgclb 13650	The property tgcl 13649 can be reversed: if the topology generated by B is actually a topology, then B must be a topological basis. This yields an alternative definition of TopBases. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( B e. TopBases <-> ( topGen ` B ) e. Top )
Theorem	tgtopon 13651	A basis generates a topology on U. B. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( B e. TopBases -> ( topGen ` B ) e. (TopOn ` U. B ) )
Theorem	topbas 13652	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
|- ( J e. Top -> J e. TopBases )
Theorem	tgtop 13653	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
|- ( J e. Top -> ( topGen ` J ) = J )
Theorem	eltop 13654	Membership in a topology, expressed without quantifiers. (Contributed by NM, 19-Jul-2006.)
|- ( J e. Top -> ( A e. J <-> A C_ U. ( J i^i ~P A ) ) )
Theorem	eltop2 13655*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|- ( J e. Top -> ( A e. J <-> A. x e. A E. y e. J ( x e. y /\ y C_ A ) ) )
Theorem	eltop3 13656*	Membership in a topology. (Contributed by NM, 19-Jul-2006.)
|- ( J e. Top -> ( A e. J <-> E. x ( x C_ J /\ A = U. x ) ) )
Theorem	tgdom 13657	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.)
|- ( B e. V -> ( topGen ` B ) ~<_ ~P B )
Theorem	tgiun 13658*	The indexed union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( ( B e. V /\ A. x e. A C e. B ) -> U_ x e. A C e. ( topGen ` B ) )
Theorem	tgidm 13659	The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- ( B e. V -> ( topGen ` ( topGen ` B ) ) = ( topGen ` B ) )
Theorem	bastop 13660	Two ways to express that a basis is a topology. (Contributed by NM, 18-Jul-2006.)
|- ( B e. TopBases -> ( B e. Top <-> ( topGen ` B ) = B ) )
Theorem	tgtop11 13661	The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006.)
|- ( ( J e. Top /\ K e. Top /\ ( topGen ` J ) = ( topGen ` K ) ) -> J = K )
Theorem	en1top 13662	{ (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
|- ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )
Theorem	tgss3 13663	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.)
|- ( ( B e. V /\ C e. W ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> B C_ ( topGen ` C ) ) )
Theorem	tgss2 13664*	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.)
|- ( ( B e. V /\ U. B = U. C ) -> ( ( topGen ` B ) C_ ( topGen ` C ) <-> A. x e. U. B A. y e. B ( x e. y -> E. z e. C ( x e. z /\ z C_ y ) ) ) )
Theorem	basgen 13665	Given a topology J, show that a subset B 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.)
|- ( ( J e. Top /\ B C_ J /\ J C_ ( topGen ` B ) ) -> ( topGen ` B ) = J )
Theorem	basgen2 13666*	Given a topology J, show that a subset B 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.)
|- ( ( J e. Top /\ B C_ J /\ A. x e. J A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) -> ( topGen ` B ) = J )
Theorem	2basgeng 13667	Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon, 5-Mar-2023.)
|- ( ( B e. V /\ B C_ C /\ C C_ ( topGen ` B ) ) -> ( topGen ` B ) = ( topGen ` C ) )
Theorem	bastop1 13668*	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 ` B ) = J " to express " B is a basis for topology J " 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.)
|- ( ( J e. Top /\ B C_ J ) -> ( ( topGen ` B ) = J <-> A. x e. J E. y ( y C_ B /\ x = U. y ) ) )
Theorem	bastop2 13669*	A version of bastop1 13668 that doesn't have B C_ J in the antecedent. (Contributed by NM, 3-Feb-2008.)
|- ( J e. Top -> ( ( topGen ` B ) = J <-> ( B C_ J /\ A. x e. J E. y ( y C_ B /\ x = U. y ) ) ) )
8.1.3  Examples of topologies
Theorem	distop 13670	The discrete topology on a set A. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro, 19-Mar-2015.)
|- ( A e. V -> ~P A e. Top )
Theorem	topnex 13671	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4451. (Contributed by BJ, 2-May-2021.)
|- Top e/ _V
Theorem	distopon 13672	The discrete topology on a set A, with base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( A e. V -> ~P A e. (TopOn ` A ) )
Theorem	sn0topon 13673	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. (TopOn ` (/) )
Theorem	sn0top 13674	The singleton of the empty set is a topology. (Contributed by Stefan Allan, 3-Mar-2006.) (Proof shortened by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. Top
Theorem	epttop 13675*	The excluded point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x -> x = A ) } e. (TopOn ` A ) )
Theorem	distps 13676	The discrete topology on a set A expressed as a topological space. (Contributed by FL, 20-Aug-2006.)
|- A e. _V   &    |- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , ~P A >. }   =>    |- K e. TopSp
8.1.4  Closure and interior
Syntax	ccld 13677	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 13678	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 13679	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 13680*	Define a function on topologies whose value is the set of closed sets of the topology. (Contributed by NM, 2-Oct-2006.)
|- Clsd = ( j e. Top |-> { x e. ~P U. j | ( U. j \ x ) e. j } )
Definition	df-ntr 13681*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 13695. (Contributed by NM, 10-Sep-2006.)
|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
Definition	df-cls 13682*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 13696. (Contributed by NM, 3-Oct-2006.)
|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
Theorem	fncld 13683	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- Clsd Fn Top
Theorem	cldval 13684*	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.)
|- X = U. J   =>    |- ( J e. Top -> ( Clsd ` J ) = { x e. ~P X | ( X \ x ) e. J } )
Theorem	ntrfval 13685*	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.)
|- X = U. J   =>    |- ( J e. Top -> ( int ` J ) = ( x e. ~P X |-> U. ( J i^i ~P x ) ) )
Theorem	clsfval 13686*	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.)
|- X = U. J   =>    |- ( J e. Top -> ( cls ` J ) = ( x e. ~P X |-> |^| { y e. ( Clsd ` J ) | x C_ y } ) )
Theorem	cldrcl 13687	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( C e. ( Clsd ` J ) -> J e. Top )
Theorem	iscld 13688	The predicate "the class S is a closed set". (Contributed by NM, 2-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( S e. ( Clsd ` J ) <-> ( S C_ X /\ ( X \ S ) e. J ) ) )
Theorem	iscld2 13689	A subset of the underlying set of a topology is closed iff its complement is open. (Contributed by NM, 4-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( X \ S ) e. J ) )
Theorem	cldss 13690	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.)
|- X = U. J   =>    |- ( S e. ( Clsd ` J ) -> S C_ X )
Theorem	cldss2 13691	The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014.)
|- X = U. J   =>    |- ( Clsd ` J ) C_ ~P X
Theorem	cldopn 13692	The complement of a closed set is open. (Contributed by NM, 5-Oct-2006.) (Revised by Stefan O'Rear, 22-Feb-2015.)
|- X = U. J   =>    |- ( S e. ( Clsd ` J ) -> ( X \ S ) e. J )
Theorem	difopn 13693	The difference of a closed set with an open set is open. (Contributed by Mario Carneiro, 6-Jan-2014.)
|- X = U. J   =>    |- ( ( A e. J /\ B e. ( Clsd ` J ) ) -> ( A \ B ) e. J )
Theorem	topcld 13694	The underlying set of a topology is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 3-Oct-2006.)
|- X = U. J   =>    |- ( J e. Top -> X e. ( Clsd ` J ) )
Theorem	ntrval 13695	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = U. ( J i^i ~P S ) )
Theorem	clsval 13696*	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = |^| { x e. ( Clsd ` J ) | S C_ x } )
Theorem	0cld 13697	The empty set is closed. Part of Theorem 6.1(1) of [Munkres] p. 93. (Contributed by NM, 4-Oct-2006.)
|- ( J e. Top -> (/) e. ( Clsd ` J ) )
Theorem	uncld 13698	The union of two closed sets is closed. Equivalent to Theorem 6.1(3) of [Munkres] p. 93. (Contributed by NM, 5-Oct-2006.)
|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A u. B ) e. ( Clsd ` J ) )
Theorem	cldcls 13699	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
|- ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
Theorem	iuncld 13700*	A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. Fin /\ A. x e. A B e. ( Clsd ` J ) ) -> U_ x e. A B e. ( Clsd ` J ) )