P. 171 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 17001-17100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bastop 17001	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 17002	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	0top 17003	The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006.)
|- ( J e. Top -> ( U. J = (/) <-> J = { (/) } ) )
Theorem	en1top 17004	{ (/) } is the only topology with one element. (Contributed by FL, 18-Aug-2008.)
|- ( J e. Top -> ( J ~~ 1o <-> J = { (/) } ) )
Theorem	en2top 17005	If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
|- ( J e. (TopOn ` X ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) )
Theorem	tgss3 17006	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 17007*	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 17008	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 17009*	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	2basgen 17010	Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- ( ( B C_ C /\ C C_ ( topGen ` B ) ) -> ( topGen ` B ) = ( topGen ` C ) )
Theorem	tgfiss 17011	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.)
|- ( ( J e. Top /\ A C_ J ) -> ( topGen ` ( fi ` A ) ) C_ J )
Theorem	tgdif0 17012	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 ` ( B \ { (/) } ) ) = ( topGen ` B )
Theorem	bastop1 17013*	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 17014*	A version of bastop1 17013 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 ) ) ) )
11.1.3  Examples of topologies
Theorem	distop 17015	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	distopon 17016	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 17017	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. (TopOn ` (/) )
Theorem	sn0top 17018	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	indislem 17019	A lemma to eliminate some sethood hypotheses when dealing with the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- { (/) , ( _I ` A ) } = { (/) , A }
Theorem	indistopon 17020	The indiscrete topology on a set A. Part of Example 2 in [Munkres] p. 77. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( A e. V -> { (/) , A } e. (TopOn ` A ) )
Theorem	indistop 17021	The indiscrete topology on a set A. 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.)
|- { (/) , A } e. Top
Theorem	indisuni 17022	The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( _I ` A ) = U. { (/) , A }
Theorem	fctop 17023*	The finite complement topology on a set A. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( A e. V -> { x e. ~P A | ( ( A \ x ) e. Fin \/ x = (/) ) } e. (TopOn ` A ) )
Theorem	fctop2 17024*	The finite complement topology on a set A. Example 3 in [Munkres] p. 77. (This version of fctop 17023 requires the Axiom of Infinity.) (Contributed by FL, 20-Aug-2006.)
|- ( A e. V -> { x e. ~P A | ( ( A \ x ) ~< om \/ x = (/) ) } e. (TopOn ` A ) )
Theorem	cctop 17025*	The countable complement topology on a set A. Example 4 in [Munkres] p. 77. (Contributed by FL, 23-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- ( A e. V -> { x e. ~P A | ( ( A \ x ) ~<_ om \/ x = (/) ) } e. (TopOn ` A ) )
Theorem	ppttop 17026*	The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x \/ x = (/) ) } e. (TopOn ` A ) )
Theorem	pptbas 17027*	The particular point topology is generated by a basis consisting of pairs { x , P } for each x e. A. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. V /\ P e. A ) -> { x e. ~P A | ( P e. x \/ x = (/) ) } = ( topGen ` ran ( x e. A |-> { x , P } ) ) )
Theorem	epttop 17028*	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	indistpsx 17029	The indiscrete topology on a set A expressed as a topological space, using explicit structure component references. Compare with indistps 17030 and indistps2 17031. The advantage of this version is that the actual function for the structure is evident, and df-ndx 13427 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 13429 and df-tset 13503 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 17030 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.)
|- A e. _V   &    |- K = { <. 1 , A >. , <. 9 , { (/) , A } >. }   =>    |- K e. TopSp
Theorem	indistps 17030	The indiscrete topology on a set A expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 17029 is that it is independent of the indices of the component definitions df-base 13429 and df-tset 13503, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 17031 is that it is easy to eliminate the hypotheses with eqid 2404 and vtoclg 2971 to result in a closed theorem. Theorems indistpsALT 17032 and indistps2ALT 17033 show that the two forms can be derived from each other. (Contributed by FL, 19-Jul-2006.)
|- A e. _V   &    |- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , { (/) , A } >. }   =>    |- K e. TopSp
Theorem	indistps2 17031	The indiscrete topology on a set A expressed as a topological space, using direct component assignments. Compare with indistps 17030. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 17032 and indistps2ALT 17033 show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012.)
|- ( Base ` K ) = A   &    |- ( TopOpen ` K ) = { (/) , A }   =>    |- K e. TopSp
Theorem	indistpsALT 17032	The indiscrete topology on a set A expressed as a topological space. Here we show how to derive the structural version indistps 17030 from the direct component assignment version indistps2 17031. (Contributed by NM, 24-Oct-2012.) (Proof modification is discouraged.)
|- A e. _V   &    |- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , { (/) , A } >. }   =>    |- K e. TopSp
Theorem	indistps2ALT 17033	The indiscrete topology on a set A expressed as a topological space, using direct component assignments. Here we show how to derive the direct component assignment version indistps2 17031 from the structural version indistps 17030. (Contributed by NM, 24-Oct-2012.) (Proof modification is discouraged.)
|- ( Base ` K ) = A   &    |- ( TopOpen ` K ) = { (/) , A }   =>    |- K e. TopSp
Theorem	distps 17034	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
11.1.4  Closure and interior
Syntax	ccld 17035	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 17036	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 17037	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 17038*	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 17039*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 17055. (Contributed by NM, 10-Sep-2006.)
|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
Definition	df-cls 17040*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 17056. (Contributed by NM, 3-Oct-2006.)
|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
Theorem	fncld 17041	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- Clsd Fn Top
Theorem	cldval 17042*	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 17043*	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 17044*	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 17045	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( C e. ( Clsd ` J ) -> J e. Top )
Theorem	iscld 17046	The predicate " 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 17047	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 17048	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 17049	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 17050	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	isopn2 17051	A subset of the underlying set of a topology is open iff its complement is closed. (Contributed by NM, 4-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. J <-> ( X \ S ) e. ( Clsd ` J ) ) )
Theorem	opncld 17052	The complement of an open set is closed. (Contributed by NM, 6-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S e. J ) -> ( X \ S ) e. ( Clsd ` J ) )
Theorem	difopn 17053	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 17054	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 17055	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 17056*	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 17057	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	iincld 17058*	The indexed intersection of a collection B ( x ) 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.)
|- ( ( A =/= (/) /\ A. x e. A B e. ( Clsd ` J ) ) -> |^|_ x e. A B e. ( Clsd ` J ) )
Theorem	intcld 17059	The intersection of a set of closed sets is closed. (Contributed by NM, 5-Oct-2006.)
|- ( ( A =/= (/) /\ A C_ ( Clsd ` J ) ) -> |^| A e. ( Clsd ` J ) )
Theorem	uncld 17060	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 17061	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
|- ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
Theorem	incld 17062	The intersection of two closed sets is closed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` J ) ) -> ( A i^i B ) e. ( Clsd ` J ) )
Theorem	riincld 17063*	An indexed relative intersection of closed sets is closed. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A. x e. A B e. ( Clsd ` J ) ) -> ( X i^i |^|_ x e. A B ) e. ( Clsd ` J ) )
Theorem	iuncld 17064*	A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- 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 17065	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	clscld 17066	The closure of a subset of a topology's underlying set is closed. (Contributed by NM, 4-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) e. ( Clsd ` J ) )
Theorem	clsf 17067	The closure function is a function from subsets of the base to closed sets. (Contributed by Mario Carneiro, 11-Apr-2015.)
|- X = U. J   =>    |- ( J e. Top -> ( cls ` J ) : ~P X --> ( Clsd ` J ) )
Theorem	ntropn 17068	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	clsval2 17069	Express closure in terms of interior. (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 \ ( ( int ` J ) ` ( X \ S ) ) ) )
Theorem	ntrval2 17070	Interior expressed in terms of closure. (Contributed by NM, 1-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( int ` J ) ` S ) = ( X \ ( ( cls ` J ) ` ( X \ S ) ) ) )
Theorem	ntrdif 17071	An interior of a complement is the complement of the closure. This set is also known as the exterior of A. (Contributed by Jeff Hankins, 31-Aug-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( ( int ` J ) ` ( X \ A ) ) = ( X \ ( ( cls ` J ) ` A ) ) )
Theorem	clsdif 17072	A closure of a complement is the complement of the interior. (Contributed by Jeff Hankins, 31-Aug-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( ( cls ` J ) ` ( X \ A ) ) = ( X \ ( ( int ` J ) ` A ) ) )
Theorem	clsss 17073	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 17074	Subset relationship for interior. (Contributed by NM, 3-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( int ` J ) ` T ) C_ ( ( int ` J ) ` S ) )
Theorem	sscls 17075	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 17076	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 17077	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	clsss3 17078	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	ntrss3 17079	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 17080	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	cmclsopn 17081	The complement of a closure is open. (Contributed by NM, 11-Sep-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( cls ` J ) ` S ) ) e. J )
Theorem	cmntrcld 17082	The complement of an interior is closed. (Contributed by NM, 1-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( int ` J ) ` S ) ) e. ( Clsd ` J ) )
Theorem	iscld3 17083	A subset is closed iff it equals its own closure. (Contributed by NM, 2-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) = S ) )
Theorem	iscld4 17084	A subset is closed iff it contains its own closure. (Contributed by NM, 31-Jan-2008.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) C_ S ) )
Theorem	isopn3 17085	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	clsidm 17086	The closure operation is idempotent. (Contributed by NM, 2-Oct-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` ( ( cls ` J ) ` S ) ) = ( ( cls ` J ) ` S ) )
Theorem	ntridm 17087	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 17088	The closure of a topology's underlying set is entire set. (Contributed by NM, 5-Oct-2007.)
|- X = U. J   =>    |- ( J e. Top -> ( ( cls ` J ) ` X ) = X )
Theorem	ntrtop 17089	The interior of a topology's underlying set is entire set. (Contributed by NM, 12-Sep-2006.)
|- X = U. J   =>    |- ( J e. Top -> ( ( int ` J ) ` X ) = X )
Theorem	0ntr 17090	A subset with an empty interior cannot cover a whole (nonempty) topology. (Contributed by NM, 12-Sep-2006.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ X =/= (/) ) /\ ( S C_ X /\ ( ( int ` J ) ` S ) = (/) ) ) -> ( X \ S ) =/= (/) )
Theorem	clsss2 17091	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	elcls 17092*	Membership in a closure. Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 22-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) )
Theorem	elcls2 17093*	Membership in a closure. (Contributed by NM, 5-Mar-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> ( P e. X /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) ) )
Theorem	clsndisj 17094	Any open set containing a point that belongs to the closure of a subset intersects the subset. One direction of Theorem 6.5(a) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ S C_ X /\ P e. ( ( cls ` J ) ` S ) ) /\ ( U e. J /\ P e. U ) ) -> ( U i^i S ) =/= (/) )
Theorem	ntrcls0 17095	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 17096*	Two ways to say that a subset has an empty 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 ) = (/) <-> A. x e. J ( x C_ S -> x = (/) ) ) )
Theorem	cldmre 17097	The closed sets of a topology comprise a Moore system on the points of the topology. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- X = U. J   =>    |- ( J e. Top -> ( Clsd ` J ) e. (Moore ` X ) )
Theorem	mrccls 17098	Moore closure generalizes closure in a topology. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- F = (mrCls ` ( Clsd ` J ) )   =>    |- ( J e. Top -> ( cls ` J ) = F )
Theorem	cls0 17099	The closure of the empty set. (Contributed by NM, 2-Oct-2007.)
|- ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )
Theorem	ntr0 17100	The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|- ( J e. Top -> ( ( int ` J ) ` (/) ) = (/) )