P. 129 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eltopss 12801	A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. J ) -> A C_ X )
8.1.1.2  Topologies on sets
Syntax	ctopon 12802	Syntax for the function of topologies on sets.
class TopOn
Definition	df-topon 12803*	Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- TopOn = ( b e. _V |-> { j e. Top | b = U. j } )
Theorem	funtopon 12804	The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.)
|- Fun TopOn
Theorem	istopon 12805	Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( J e. (TopOn ` B ) <-> ( J e. Top /\ B = U. J ) )
Theorem	topontop 12806	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	toponuni 12807	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	topontopi 12808	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 12809	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 12810	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 12811	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 12812	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 12813	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 12814	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 12815	The domain of TopOn is _V. (Contributed by BJ, 29-Apr-2021.)
|- dom TopOn = _V
Theorem	fntopon 12816	The class TopOn is a function with domain _V. (Contributed by BJ, 29-Apr-2021.)
|- TopOn Fn _V
Theorem	toponmax 12817	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 12818	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 12819	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 12820	Biconditional form of toponcom 12819. (Contributed by BJ, 5-Dec-2021.)
|- ( ( J e. Top /\ K e. Top ) -> ( J e. (TopOn ` U. K ) <-> K e. (TopOn ` U. J ) ) )
Theorem	topgele 12821	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 12822	Syntax for the class of topological spaces.
class TopSp
Definition	df-topsp 12823	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 12824	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 12825	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 12826	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 12827	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 12828	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 12829	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 12830	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 12831	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 12832	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 12833	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 12834	Syntax for the class of topological bases.
class TopBases
Definition	df-bases 12835*	Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 12837). 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 12836*	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 12837*	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 12838*	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 12839	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 12840*	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 12841*	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 12842*	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	tgval 12843*	The topology generated by a basis. See also tgval2 12845 and tgval3 12852. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.)
|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )
Theorem	tgvalex 12844	The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.)
|- ( B e. V -> ( topGen ` B ) e. _V )
Theorem	tgval2 12845*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 12858) that ( topGen ` B ) is indeed a topology (on U. B, see unitg 12856). See also tgval 12843 and tgval3 12852. (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 12846	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 12847*	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 12848*	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 12849	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 12850	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 12851*	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 12852*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 12843 and tgval2 12845. (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 12853	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 12854*	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 12855	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 12856	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 12857	Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
|- ( ( C e. V /\ B C_ C ) -> ( topGen ` B ) C_ ( topGen ` C ) )
Theorem	tgcl 12858	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 12859	The property tgcl 12858 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 12860	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 12861	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
|- ( J e. Top -> J e. TopBases )
Theorem	tgtop 12862	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
|- ( J e. Top -> ( topGen ` J ) = J )
Theorem	eltop 12863	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 12864*	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 12865*	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 12866	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 12867*	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 12868	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 12869	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 12870	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 12871	{ (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
|- ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )
Theorem	tgss3 12872	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 12873*	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 12874	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 12875*	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 12876	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 12877*	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 12878*	A version of bastop1 12877 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 12879	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 12880	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4434. (Contributed by BJ, 2-May-2021.)
|- Top e/ _V
Theorem	distopon 12881	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 12882	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. (TopOn ` (/) )
Theorem	sn0top 12883	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 12884*	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 12885	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 12886	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 12887	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 12888	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 12889*	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 12890*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 12904. (Contributed by NM, 10-Sep-2006.)
|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
Definition	df-cls 12891*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 12905. (Contributed by NM, 3-Oct-2006.)
|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
Theorem	fncld 12892	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- Clsd Fn Top
Theorem	cldval 12893*	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 12894*	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 12895*	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 12896	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( C e. ( Clsd ` J ) -> J e. Top )
Theorem	iscld 12897	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 12898	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 12899	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 12900	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