P. 143 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14201-14300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	istps2 14201	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 14202	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 14203	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 14204	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 14205	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 14206	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 14207	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 14208	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 14209	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
9.1.2  Topological bases
Syntax	ctb 14210	Syntax for the class of topological bases.
class TopBases
Definition	df-bases 14211*	Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 14213). 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 14212*	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 14213*	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 14214*	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 14215	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 14216*	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 14217*	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 14218*	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 14219*	Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 14232) that ( topGen ` B ) is indeed a topology (on U. B, see unitg 14230). See also tgval 12873 and tgval3 14226. (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 14220	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 14221*	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 14222*	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 14223	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 14224	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 14225*	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 14226*	Alternate expression for the topology generated by a basis. Lemma 2.1 of [Munkres] p. 80. See also tgval 12873 and tgval2 14219. (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 14227	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 14228*	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 14229	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 14230	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 14231	Subset relation for generated topologies. (Contributed by NM, 7-May-2007.)
|- ( ( C e. V /\ B C_ C ) -> ( topGen ` B ) C_ ( topGen ` C ) )
Theorem	tgcl 14232	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 14233	The property tgcl 14232 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 14234	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 14235	A topology is its own basis. (Contributed by NM, 17-Jul-2006.)
|- ( J e. Top -> J e. TopBases )
Theorem	tgtop 14236	A topology is its own basis. (Contributed by NM, 18-Jul-2006.)
|- ( J e. Top -> ( topGen ` J ) = J )
Theorem	eltop 14237	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 14238*	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 14239*	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 14240	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 14241*	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 14242	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 14243	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 14244	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 14245	{ (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
|- ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )
Theorem	tgss3 14246	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 14247*	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 14248	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 14249*	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 14250	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 14251*	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 14252*	A version of bastop1 14251 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 ) ) ) )
9.1.3  Examples of topologies
Theorem	distop 14253	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 14254	The class of all topologies is a proper class. The proof uses discrete topologies and pwnex 4480. (Contributed by BJ, 2-May-2021.)
|- Top e/ _V
Theorem	distopon 14255	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 14256	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. (TopOn ` (/) )
Theorem	sn0top 14257	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 14258*	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 14259	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
9.1.4  Closure and interior
Syntax	ccld 14260	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 14261	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 14262	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 14263*	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 14264*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 14278. (Contributed by NM, 10-Sep-2006.)
|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
Definition	df-cls 14265*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 14279. (Contributed by NM, 3-Oct-2006.)
|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
Theorem	fncld 14266	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- Clsd Fn Top
Theorem	cldval 14267*	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 14268*	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 14269*	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 14270	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( C e. ( Clsd ` J ) -> J e. Top )
Theorem	iscld 14271	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 14272	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 14273	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 14274	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 14275	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 14276	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 14277	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 14278	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 14279*	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 14280	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 14281	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 14282	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
|- ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
Theorem	iuncld 14283*	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 ) )
Theorem	unicld 14284	A finite union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. Fin /\ A C_ ( Clsd ` J ) ) -> U. A e. ( Clsd ` J ) )
Theorem	ntropn 14285	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) e. J )
Theorem	clsss 14286	Subset relationship for closure. (Contributed by NM, 10-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( cls ` J ) ` T ) C_ ( ( cls ` J ) ` S ) )
Theorem	ntrss 14287	Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( int ` J ) ` T ) C_ ( ( int ` J ) ` S ) )
Theorem	sscls 14288	A subset of a topology's underlying set is included in its closure. (Contributed by NM, 22-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )
Theorem	ntrss2 14289	A subset includes its interior. (Contributed by NM, 3-Oct-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ S )
Theorem	ssntr 14290	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.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ S C_ X ) /\ ( O e. J /\ O C_ S ) ) -> O C_ ( ( int ` J ) ` S ) )
Theorem	ntrss3 14291	The interior of a subset of a topological space is included in the space. (Contributed by NM, 1-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) C_ X )
Theorem	ntrin 14292	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.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X /\ B C_ X ) -> ( ( int ` J ) ` ( A i^i B ) ) = ( ( ( int ` J ) ` A ) i^i ( ( int ` J ) ` B ) ) )
Theorem	isopn3 14293	A subset is open iff it equals its own interior. (Contributed by NM, 9-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. J <-> ( ( int ` J ) ` S ) = S ) )
Theorem	ntridm 14294	The interior operation is idempotent. (Contributed by NM, 2-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` ( ( int ` J ) ` S ) ) = ( ( int ` J ) ` S ) )
Theorem	clstop 14295	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.)
|- X = U. J   =>    |- ( J e. Top -> ( ( cls ` J ) ` X ) = X )
Theorem	ntrtop 14296	The interior of a topology's underlying set is the entire set. (Contributed by NM, 12-Sep-2006.)
|- X = U. J   =>    |- ( J e. Top -> ( ( int ` J ) ` X ) = X )
Theorem	clsss2 14297	If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007.)
|- X = U. J   =>    |- ( ( C e. ( Clsd ` J ) /\ S C_ C ) -> ( ( cls ` J ) ` S ) C_ C )
Theorem	clsss3 14298	The closure of a subset of a topological space is included in the space. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
Theorem	ntrcls0 14299	A subset whose closure has an empty interior also has an empty interior. (Contributed by NM, 4-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ ( ( int ` J ) ` ( ( cls ` J ) ` S ) ) = (/) ) -> ( ( int ` J ) ` S ) = (/) )
Theorem	ntreq0 14300*	Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( ( int ` J ) ` S ) = (/) <-> A. x e. J ( x C_ S -> x = (/) ) ) )