P. 209 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20801-20900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	distopon 20801	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 20802	The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- { (/) } e. (TopOn ` (/) )
Theorem	sn0top 20803	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 20804	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 20805	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 20806	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 20807	The base set of the indiscrete topology. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( _I ` A ) = U. { (/) , A }
Theorem	fctop 20808*	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 20809*	The finite complement topology on a set A. Example 3 in [Munkres] p. 77. (This version of fctop 20808 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 20810*	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 20811*	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 20812*	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 20813*	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 20814	The indiscrete topology on a set A expressed as a topological space, using explicit structure component references. Compare with indistps 20815 and indistps2 20816. The advantage of this version is that the actual function for the structure is evident, and df-ndx 15860 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 15863 and df-tset 15960 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 20815 instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006.)
|- A e. _V   &    |- K = { <. 1 , A >. , <. 9 , { (/) , A } >. }   =>    |- K e. TopSp
Theorem	indistps 20815	The indiscrete topology on a set A expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx 20814 is that it is independent of the indices of the component definitions df-base 15863 and df-tset 15960, and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 20816 is that it is easy to eliminate the hypotheses with eqid 2622 and vtoclg 3266 to result in a closed theorem. Theorems indistpsALT 20817 and indistps2ALT 20818 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 20816	The indiscrete topology on a set A expressed as a topological space, using direct component assignments. Compare with indistps 20815. The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT 20817 and indistps2ALT 20818 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 20817	The indiscrete topology on a set A expressed as a topological space. Here we show how to derive the structural version indistps 20815 from the direct component assignment version indistps2 20816. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- K = { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , { (/) , A } >. }   =>    |- K e. TopSp
Theorem	indistps2ALT 20818	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 20816 from the structural version indistps 20815. (Contributed by NM, 24-Oct-2012.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( Base ` K ) = A   &    |- ( TopOpen ` K ) = { (/) , A }   =>    |- K e. TopSp
Theorem	distps 20819	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
12.1.4  Closure and interior
Syntax	ccld 20820	Extend class notation with the set of closed sets of a topology.
class Clsd
Syntax	cnt 20821	Extend class notation with interior of a subset of a topology base set.
class int
Syntax	ccl 20822	Extend class notation with closure of a subset of a topology base set.
class cls
Definition	df-cld 20823*	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 20824*	Define a function on topologies whose value is the interior function on the subsets of the base set. See ntrval 20840. (Contributed by NM, 10-Sep-2006.)
|- int = ( j e. Top |-> ( x e. ~P U. j |-> U. ( j i^i ~P x ) ) )
Definition	df-cls 20825*	Define a function on topologies whose value is the closure function on the subsets of the base set. See clsval 20841. (Contributed by NM, 3-Oct-2006.)
|- cls = ( j e. Top |-> ( x e. ~P U. j |-> |^| { y e. ( Clsd ` j ) | x C_ y } ) )
Theorem	fncld 20826	The closed-set generator is a well-behaved function. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- Clsd Fn Top
Theorem	cldval 20827*	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 20828*	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 20829*	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 20830	Reverse closure of the closed set operation. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( C e. ( Clsd ` J ) -> J e. Top )
Theorem	iscld 20831	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 20832	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 20833	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 20834	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 20835	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 20836	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 20837	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 20838	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 20839	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 20840	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 20841*	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 20842	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 20843*	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 20844	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 20845	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 20846	A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007.)
|- ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
Theorem	incld 20847	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 20848*	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 20849*	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 20850	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 20851	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 20852	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 20853	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 20854	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 20855	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 20856	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 20857	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 20858	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 20859	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 20860	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 20861	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 20862	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 20863	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 20864	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 20865	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 20866	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 20867	The complement of an interior is closed. (Contributed by NM, 1-Oct-2007.) (Proof shortened by OpenAI, 3-Jul-2020.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( X \ ( ( int ` J ) ` S ) ) e. ( Clsd ` J ) )
Theorem	iscld3 20868	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 20869	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 20870	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 20871	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 20872	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 20873	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 20874	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 20875	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 20876	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 20877*	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 20878*	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 20879	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 20880	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 20881*	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 20882	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 20883	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 20884	The closure of the empty set. (Contributed by NM, 2-Oct-2007.)
|- ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )
Theorem	ntr0 20885	The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|- ( J e. Top -> ( ( int ` J ) ` (/) ) = (/) )
Theorem	isopn3i 20886	An open subset equals its own interior. (Contributed by Mario Carneiro, 30-Dec-2016.)
|- ( ( J e. Top /\ S e. J ) -> ( ( int ` J ) ` S ) = S )
Theorem	elcls3 20887*	Membership in a closure in terms of the members of a basis. Theorem 6.5(b) of [Munkres] p. 95. (Contributed by NM, 26-Feb-2007.) (Revised by Mario Carneiro, 3-Sep-2015.)
|- ( ph -> J = ( topGen ` B ) )   &    |- ( ph -> X = U. J )   &    |- ( ph -> B e. TopBases )   &    |- ( ph -> S C_ X )   &    |- ( ph -> P e. X )   =>    |- ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. B ( P e. x -> ( x i^i S ) =/= (/) ) ) )
Theorem	opncldf1 20888*	A bijection useful for converting statements about open sets to statements about closed sets and vice versa. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
|- X = U. J   &    |- F = ( u e. J |-> ( X \ u ) )   =>    |- ( J e. Top -> ( F : J -1-1-onto-> ( Clsd ` J ) /\ `' F = ( x e. ( Clsd ` J ) |-> ( X \ x ) ) ) )
Theorem	opncldf2 20889*	The values of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
|- X = U. J   &    |- F = ( u e. J |-> ( X \ u ) )   =>    |- ( ( J e. Top /\ A e. J ) -> ( F ` A ) = ( X \ A ) )
Theorem	opncldf3 20890*	The values of the converse/inverse of the open-closed bijection. (Contributed by Jeff Hankins, 27-Aug-2009.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)
|- X = U. J   &    |- F = ( u e. J |-> ( X \ u ) )   =>    |- ( B e. ( Clsd ` J ) -> ( `' F ` B ) = ( X \ B ) )
Theorem	isclo 20891*	A set A is clopen iff for every point x in the space there is a neighborhood y such that all the points in y are in A iff x is. (Contributed by Mario Carneiro, 10-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( A e. ( J i^i ( Clsd ` J ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( x e. A <-> z e. A ) ) ) )
Theorem	isclo2 20892*	A set A is clopen iff for every point x in the space there is a neighborhood y of x which is either disjoint from A or contained in A. (Contributed by Mario Carneiro, 7-Jul-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> ( A e. ( J i^i ( Clsd ` J ) ) <-> A. x e. X E. y e. J ( x e. y /\ A. z e. y ( z e. A -> y C_ A ) ) ) )
Theorem	discld 20893	The open sets of a discrete topology are closed and its closed sets are open. (Contributed by FL, 7-Jun-2007.) (Revised by Mario Carneiro, 7-Apr-2015.)
|- ( A e. V -> ( Clsd ` ~P A ) = ~P A )
Theorem	sn0cld 20894	The closed sets of the topology { (/) }. (Contributed by FL, 5-Jan-2009.)
|- ( Clsd ` { (/) } ) = { (/) }
Theorem	indiscld 20895	The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( Clsd ` { (/) , A } ) = { (/) , A }
Theorem	mretopd 20896*	A Moore collection which is closed under finite unions called topological; such a collection is the closed sets of a canonically associated topology. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> M e. (Moore ` B ) )   &    |- ( ph -> (/) e. M )   &    |- ( ( ph /\ x e. M /\ y e. M ) -> ( x u. y ) e. M )   &    |- J = { z e. ~P B | ( B \ z ) e. M }   =>    |- ( ph -> ( J e. (TopOn ` B ) /\ M = ( Clsd ` J ) ) )
Theorem	toponmre 20897	The topologies over a given base set form a Moore collection: the intersection of any family of them is a topology, including the empty (relative) intersection which gives the discrete topology distop 20799. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 5-May-2015.)
|- ( B e. V -> (TopOn ` B ) e. (Moore ` ~P B ) )
Theorem	cldmreon 20898	The closed sets of a topology over a set are a Moore collection over the same set. (Contributed by Stefan O'Rear, 31-Jan-2015.)
|- ( J e. (TopOn ` B ) -> ( Clsd ` J ) e. (Moore ` B ) )
Theorem	iscldtop 20899*	A family is the closed sets of a topology iff it is a Moore collection and closed under finite union. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( K e. ( Clsd " (TopOn ` B ) ) <-> ( K e. (Moore ` B ) /\ (/) e. K /\ A. x e. K A. y e. K ( x u. y ) e. K ) )
Theorem	mreclatdemoBAD 20900	The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD 17187. (Contributed by Stefan O'Rear, 31-Jan-2015.) TODO (df-riota 6611 update): This proof uses the old df-clat 17108 and references the required instance of mreclatBAD 17187 as a hypothesis. When mreclatBAD 17187 is corrected to become mreclat, delete this theorem and uncomment the mreclatdemo below.
|- ( ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. (Moore ` U. ( TopOpen ` W ) ) -> (toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )   =>    |- ( W e. ( TopSp i^i LMod ) -> (toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )