P. 210 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20901-21000   *Has distinct variable group(s)

Type	Label	Description
Statement
12.1.5  Neighborhoods
Syntax	cnei 20901	Extend class notation with neighborhood relation for topologies.
class nei
Definition	df-nei 20902*	Define a function on topologies whose value is a map from a subset to its neighborhoods. (Contributed by NM, 11-Feb-2007.)
|- nei = ( j e. Top |-> ( x e. ~P U. j |-> { y e. ~P U. j | E. g e. j ( x C_ g /\ g C_ y ) } ) )
Theorem	neifval 20903*	The neighborhood function on the subsets of a topology's base set. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )
Theorem	neif 20904	The neighborhood function is a function of the subsets of a topology's base set. (Contributed by NM, 12-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( nei ` J ) Fn ~P X )
Theorem	neiss2 20905	A set with a neighborhood is a subset of the topology's base set. (This theorem depends on a function's value being empty outside of its domain, but it will make later theorems simpler to state.) (Contributed by NM, 12-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ X )
Theorem	neival 20906*	The set of neighborhoods of a subset of the base set of a topology. (Contributed by NM, 11-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( nei ` J ) ` S ) = { v e. ~P X | E. g e. J ( S C_ g /\ g C_ v ) } )
Theorem	isnei 20907*	The predicate " N is a neighborhood of S." (Contributed by FL, 25-Sep-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> ( N C_ X /\ E. g e. J ( S C_ g /\ g C_ N ) ) ) )
Theorem	neiint 20908	An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ N C_ X ) -> ( N e. ( ( nei ` J ) ` S ) <-> S C_ ( ( int ` J ) ` N ) ) )
Theorem	isneip 20909*	The predicate " N is a neighborhood of point P." (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ P e. X ) -> ( N e. ( ( nei ` J ) ` { P } ) <-> ( N C_ X /\ E. g e. J ( P e. g /\ g C_ N ) ) ) )
Theorem	neii1 20910	A neighborhood is included in the topology's base set. (Contributed by NM, 12-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> N C_ X )
Theorem	neisspw 20911	The neighborhoods of any set are subsets of the base set. (Contributed by Stefan O'Rear, 6-Aug-2015.)
|- X = U. J   =>    |- ( J e. Top -> ( ( nei ` J ) ` S ) C_ ~P X )
Theorem	neii2 20912*	Property of a neighborhood. (Contributed by NM, 12-Feb-2007.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. g e. J ( S C_ g /\ g C_ N ) )
Theorem	neiss 20913	Any neighborhood of a set S is also a neighborhood of any subset R C_ S. Theorem of [BourbakiTop1] p. I.2. (Contributed by FL, 25-Sep-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ R C_ S ) -> N e. ( ( nei ` J ) ` R ) )
Theorem	ssnei 20914	A set is included in its neighborhoods. Proposition Viii of [BourbakiTop1] p. I.3 . (Contributed by FL, 16-Nov-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N )
Theorem	elnei 20915	A point belongs to any of its neighborhoods. Proposition Viii of [BourbakiTop1] p. I.3. (Contributed by FL, 28-Sep-2006.)
|- ( ( J e. Top /\ P e. A /\ N e. ( ( nei ` J ) ` { P } ) ) -> P e. N )
Theorem	0nnei 20916	The empty set is not a neighborhood of a nonempty set. (Contributed by FL, 18-Sep-2007.)
|- ( ( J e. Top /\ S =/= (/) ) -> -. (/) e. ( ( nei ` J ) ` S ) )
Theorem	neips 20917*	A neighborhood of a set is a neighborhood of every point in the set. Proposition of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ S =/= (/) ) -> ( N e. ( ( nei ` J ) ` S ) <-> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )
Theorem	opnneissb 20918	An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( ( J e. Top /\ N e. J /\ S C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
Theorem	opnssneib 20919	Any superset of an open set is a neighborhood of it. (Contributed by NM, 14-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S e. J /\ N C_ X ) -> ( S C_ N <-> N e. ( ( nei ` J ) ` S ) ) )
Theorem	ssnei2 20920	Any subset of X containing a neighborhood of a set is a neighborhood of this set. Proposition Vi of [BourbakiTop1] p. I.3. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) /\ ( N C_ M /\ M C_ X ) ) -> M e. ( ( nei ` J ) ` S ) )
Theorem	neindisj 20921	Any neighborhood of an element in the closure of a subset intersects the subset. Part of proof of Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ S C_ X ) /\ ( P e. ( ( cls ` J ) ` S ) /\ N e. ( ( nei ` J ) ` { P } ) ) ) -> ( N i^i S ) =/= (/) )
Theorem	opnneiss 20922	An open set is a neighborhood of any of its subsets. (Contributed by NM, 13-Feb-2007.)
|- ( ( J e. Top /\ N e. J /\ S C_ N ) -> N e. ( ( nei ` J ) ` S ) )
Theorem	opnneip 20923	An open set is a neighborhood of any of its members. (Contributed by NM, 8-Mar-2007.)
|- ( ( J e. Top /\ N e. J /\ P e. N ) -> N e. ( ( nei ` J ) ` { P } ) )
Theorem	opnnei 20924*	A set is open iff it is a neighborhood of all of its points. (Contributed by Jeff Hankins, 15-Sep-2009.)
|- ( J e. Top -> ( S e. J <-> A. x e. S S e. ( ( nei ` J ) ` { x } ) ) )
Theorem	tpnei 20925	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 20922. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )
Theorem	neiuni 20926	The union of the neighborhoods of a set equals the topology's underlying set. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> X = U. ( ( nei ` J ) ` S ) )
Theorem	neindisj2 20927*	A point P belongs to the closure of a set S iff every neighborhood of P meets S. (Contributed by FL, 15-Sep-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i S ) =/= (/) ) )
Theorem	topssnei 20928	A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top /\ X = Y ) /\ J C_ K ) -> ( ( nei ` J ) ` S ) C_ ( ( nei ` K ) ` S ) )
Theorem	innei 20929	The intersection of two neighborhoods of a set is also a neighborhood of the set. Proposition Vii of [BourbakiTop1] p. I.3 . (Contributed by FL, 28-Sep-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) /\ M e. ( ( nei ` J ) ` S ) ) -> ( N i^i M ) e. ( ( nei ` J ) ` S ) )
Theorem	opnneiid 20930	Only an open set is a neighborhood of itself. (Contributed by FL, 2-Oct-2006.)
|- ( J e. Top -> ( N e. ( ( nei ` J ) ` N ) <-> N e. J ) )
Theorem	neissex 20931*	For any neighborhood N of S, there is a neighborhood x of S such that N is a neighborhood of all subsets of x. Proposition Viv of [BourbakiTop1] p. I.3 . (Contributed by FL, 2-Oct-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> E. x e. ( ( nei ` J ) ` S ) A. y ( y C_ x -> N e. ( ( nei ` J ) ` y ) ) )
Theorem	0nei 20932	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
|- ( J e. Top -> (/) e. ( ( nei ` J ) ` (/) ) )
Theorem	neipeltop 20933*	Lemma for neiptopreu 20937. (Contributed by Thierry Arnoux, 6-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   =>    |- ( C e. J <-> ( C C_ X /\ A. p e. C C e. ( N ` p ) ) )
Theorem	neiptopuni 20934*	Lemma for neiptopreu 20937. (Contributed by Thierry Arnoux, 6-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> X = U. J )
Theorem	neiptoptop 20935*	Lemma for neiptopreu 20937. (Contributed by Thierry Arnoux, 7-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> J e. Top )
Theorem	neiptopnei 20936*	Lemma for neiptopreu 20937. (Contributed by Thierry Arnoux, 7-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> N = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) )
Theorem	neiptopreu 20937*	If, to each element P of a set X, we associate a set ( N ` P ) fulfilling the properties Vi, Vii, Viii and property Viv of [BourbakiTop1] p. I.2. , corresponding to ssnei 20914, innei 20929, elnei 20915 and neissex 20931, then there is a unique topology j such that for any point p, ( N ` p ) is the set of neighborhoods of p. Proposition 2 of [BourbakiTop1] p. I.3. This can be used to build a topology from a set of neighborhoods. Note that the additional condition that X is a neighborhood of all points was added. (Contributed by Thierry Arnoux, 6-Jan-2018.)
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }   &    |- ( ph -> N : X --> ~P ~P X )   &    |- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )   &    |- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )   &    |- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )   &    |- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )   =>    |- ( ph -> E! j e. (TopOn ` X ) N = ( p e. X |-> ( ( nei ` j ) ` { p } ) ) )
12.1.6  Limit points and perfect sets
Syntax	clp 20938	Extend class notation with the limit point function for topologies.
class limPt
Syntax	cperf 20939	Extend class notation with the class of all perfect spaces.
class Perf
Definition	df-lp 20940*	Define a function on topologies whose value is the set of limit points of the subsets of the base set. See lpval 20943. (Contributed by NM, 10-Feb-2007.)
|- limPt = ( j e. Top |-> ( x e. ~P U. j |-> { y | y e. ( ( cls ` j ) ` ( x \ { y } ) ) } ) )
Definition	df-perf 20941	Define the class of all perfect spaces. A perfect space is one for which every point in the set is a limit point of the whole space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- Perf = { j e. Top | ( ( limPt ` j ) ` U. j ) = U. j }
Theorem	lpfval 20942*	The limit point function on the subsets of a topology's base set. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( J e. Top -> ( limPt ` J ) = ( x e. ~P X |-> { y | y e. ( ( cls ` J ) ` ( x \ { y } ) ) } ) )
Theorem	lpval 20943*	The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in [Munkres] p. 97. (Contributed by NM, 10-Feb-2007.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) = { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } )
Theorem	islp 20944	The predicate " P is a limit point of S." (Contributed by NM, 10-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) ) )
Theorem	lpsscls 20945	The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) C_ ( ( cls ` J ) ` S ) )
Theorem	lpss 20946	The limit points of a subset are included in the base set. (Contributed by NM, 9-Nov-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) C_ X )
Theorem	lpdifsn 20947	P is a limit point of S iff it is a limit point of S \ { P }. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( limPt ` J ) ` ( S \ { P } ) ) ) )
Theorem	lpss3 20948	Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ T C_ S ) -> ( ( limPt ` J ) ` T ) C_ ( ( limPt ` J ) ` S ) )
Theorem	islp2 20949*	The predicate " P is a limit point of S," in terms of neighborhoods. Definition of limit point in [Munkres] p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods. (Contributed by NM, 26-Feb-2007.) (Proof shortened by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { P } ) ( n i^i ( S \ { P } ) ) =/= (/) ) )
Theorem	islp3 20950*	The predicate " P is a limit point of S " in terms of open sets. see islp2 20949, elcls 20877, islp 20944. (Contributed by FL, 31-Jul-2009.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i ( S \ { P } ) ) =/= (/) ) ) )
Theorem	maxlp 20951	A point is a limit point of the whole space iff the singleton of the point is not open. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Top -> ( P e. ( ( limPt ` J ) ` X ) <-> ( P e. X /\ -. { P } e. J ) ) )
Theorem	clslp 20952	The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( S u. ( ( limPt ` J ) ` S ) ) )
Theorem	islpi 20953	A point belonging to a set's closure but not the set itself is a limit point. (Contributed by NM, 8-Nov-2007.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ S C_ X ) /\ ( P e. ( ( cls ` J ) ` S ) /\ -. P e. S ) ) -> P e. ( ( limPt ` J ) ` S ) )
Theorem	cldlp 20954	A subset of a topological space is closed iff it contains all its limit points. Corollary 6.7 of [Munkres] p. 97. (Contributed by NM, 26-Feb-2007.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( limPt ` J ) ` S ) C_ S ) )
Theorem	isperf 20955	Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) )
Theorem	isperf2 20956	Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) )
Theorem	isperf3 20957*	A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )
Theorem	perflp 20958	The limit points of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( J e. Perf -> ( ( limPt ` J ) ` X ) = X )
Theorem	perfi 20959	Property of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Perf /\ P e. X ) -> -. { P } e. J )
Theorem	perftop 20960	A perfect space is a topology. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- ( J e. Perf -> J e. Top )
12.1.7  Subspace topologies
Theorem	restrcl 20961	Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J ↾t A ) e. Top -> ( J e. _V /\ A e. _V ) )
Theorem	restbas 20962	A subspace topology basis is a basis. Y is normally a subset of the base set of J. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( B e. TopBases -> ( B ↾t A ) e. TopBases )
Theorem	tgrest 20963	A subspace can be generated by restricted sets from a basis for the original topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Mario Carneiro, 30-Aug-2015.)
|- ( ( B e. V /\ A e. W ) -> ( topGen ` ( B ↾t A ) ) = ( ( topGen ` B ) ↾t A ) )
Theorem	resttop 20964	A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. A is normally a subset of the base set of J. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. Top /\ A e. V ) -> ( J ↾t A ) e. Top )
Theorem	resttopon 20965	A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A C_ X ) -> ( J ↾t A ) e. (TopOn ` A ) )
Theorem	restuni 20966	The underlying set of a subspace topology. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> A = U. ( J ↾t A ) )
Theorem	stoig 20967	The topological space built with a subspace topology. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X ) -> { <. ( Base ` ndx ) , A >. , <. (TopSet ` ndx ) , ( J ↾t A ) >. } e. TopSp )
Theorem	restco 20968	Composition of subspaces. (Contributed by Mario Carneiro, 15-Dec-2013.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ A e. W /\ B e. X ) -> ( ( J ↾t A ) ↾t B ) = ( J ↾t ( A i^i B ) ) )
Theorem	restabs 20969	Equivalence of being a subspace of a subspace and being a subspace of the original. (Contributed by Jeff Hankins, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 1-May-2015.)
|- ( ( J e. V /\ S C_ T /\ T e. W ) -> ( ( J ↾t T ) ↾t S ) = ( J ↾t S ) )
Theorem	restin 20970	When the subspace region is not a subset of the base of the topology, the resulting set is the same as the subspace restricted to the base. (Contributed by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   =>    |- ( ( J e. V /\ A e. W ) -> ( J ↾t A ) = ( J ↾t ( A i^i X ) ) )
Theorem	restuni2 20971	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- X = U. J   =>    |- ( ( J e. Top /\ A e. V ) -> ( A i^i X ) = U. ( J ↾t A ) )
Theorem	resttopon2 20972	The underlying set of a subspace topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. V ) -> ( J ↾t A ) e. (TopOn ` ( A i^i X ) ) )
Theorem	rest0 20973	The subspace topology induced by the topology J on the empty set. (Contributed by FL, 22-Dec-2008.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( J e. Top -> ( J ↾t (/) ) = { (/) } )
Theorem	restsn 20974	The only subspace topology induced by the topology { (/) }. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- ( A e. V -> ( { (/) } ↾t A ) = { (/) } )
Theorem	restsn2 20975	The subspace topology induced by a singleton. (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. X ) -> ( J ↾t { A } ) = ~P { A } )
Theorem	restcld 20976*	A closed set of a subspace topology is a closed set of the original topology intersected with the subset. (Contributed by FL, 11-Jul-2009.) (Proof shortened by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X ) -> ( A e. ( Clsd ` ( J ↾t S ) ) <-> E. x e. ( Clsd ` J ) A = ( x i^i S ) ) )
Theorem	restcldi 20977	A closed set is closed in the subspace topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- X = U. J   =>    |- ( ( A C_ X /\ B e. ( Clsd ` J ) /\ B C_ A ) -> B e. ( Clsd ` ( J ↾t A ) ) )
Theorem	restcldr 20978	A set which is closed in the subspace topology induced by a closed set is closed in the original topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( A e. ( Clsd ` J ) /\ B e. ( Clsd ` ( J ↾t A ) ) ) -> B e. ( Clsd ` J ) )
Theorem	restopnb 20979	If B is an open subset of the subspace base set A, then any subset of B is open iff it is open in A. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- ( ( ( J e. Top /\ A e. V ) /\ ( B e. J /\ B C_ A /\ C C_ B ) ) -> ( C e. J <-> C e. ( J ↾t A ) ) )
Theorem	ssrest 20980	If K is a finer topology than J, then the subspace topologies induced by A maintain this relationship. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 1-May-2015.)
|- ( ( K e. V /\ J C_ K ) -> ( J ↾t A ) C_ ( K ↾t A ) )
Theorem	restopn2 20981	The if A is open, then B is open in A iff it is an open subset of A. (Contributed by Mario Carneiro, 2-Mar-2015.)
|- ( ( J e. Top /\ A e. J ) -> ( B e. ( J ↾t A ) <-> ( B e. J /\ B C_ A ) ) )
Theorem	restdis 20982	A subspace of a discrete topology is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( A e. V /\ B C_ A ) -> ( ~P A ↾t B ) = ~P B )
Theorem	restfpw 20983	The restriction of the set of finite subsets of A is the set of finite subsets of B. (Contributed by Mario Carneiro, 18-Sep-2015.)
|- ( ( A e. V /\ B C_ A ) -> ( ( ~P A i^i Fin ) ↾t B ) = ( ~P B i^i Fin ) )
Theorem	neitr 20984	The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018.)
|- X = U. J   =>    |- ( ( J e. Top /\ A C_ X /\ B C_ A ) -> ( ( nei ` ( J ↾t A ) ) ` B ) = ( ( ( nei ` J ) ` B ) ↾t A ) )
Theorem	restcls 20985	A closure in a subspace topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` K ) ` S ) = ( ( ( cls ` J ) ` S ) i^i Y ) )
Theorem	restntr 20986	An interior in a subspace topology. Willard in General Topology says that there is no analogue of restcls 20985 for interiors. In some sense, that is true. (Contributed by Jeff Hankins, 23-Jan-2010.) (Revised by Mario Carneiro, 15-Dec-2013.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( int ` K ) ` S ) = ( ( ( int ` J ) ` ( S u. ( X \ Y ) ) ) i^i Y ) )
Theorem	restlp 20987	The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( limPt ` K ) ` S ) = ( ( ( limPt ` J ) ` S ) i^i Y ) )
Theorem	restperf 20988	Perfection of a subspace. Note that the term "perfect set" is reserved for closed sets which are perfect in the subspace topology. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Top /\ Y C_ X ) -> ( K e. Perf <-> Y C_ ( ( limPt ` J ) ` Y ) ) )
Theorem	perfopn 20989	An open subset of a perfect space is perfect. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   &    |- K = ( J ↾t Y )   =>    |- ( ( J e. Perf /\ Y e. J ) -> K e. Perf )
Theorem	resstopn 20990	The topology of a restricted structure. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- H = ( K ↾s A )   &    |- J = ( TopOpen ` K )   =>    |- ( J ↾t A ) = ( TopOpen ` H )
Theorem	resstps 20991	A restricted topological space is a topological space. Note that this theorem would not be true if TopSp was defined directly in terms of the TopSet slot instead of the TopOpen derived function. (Contributed by Mario Carneiro, 13-Aug-2015.)
|- ( ( K e. TopSp /\ A e. V ) -> ( K ↾s A ) e. TopSp )
12.1.8  Order topology
Theorem	ordtbaslem 20992*	Lemma for ordtbas 20996. In a total order, unbounded-above intervals are closed under intersection. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   &    |- A = ran ( x e. X |-> { y e. X | -. y R x } )   =>    |- ( R e. TosetRel -> ( fi ` A ) = A )
Theorem	ordtval 20993*	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   &    |- A = ran ( x e. X |-> { y e. X | -. y R x } )   &    |- B = ran ( x e. X |-> { y e. X | -. x R y } )   =>    |- ( R e. V -> (ordTop ` R ) = ( topGen ` ( fi ` ( { X } u. ( A u. B ) ) ) ) )
Theorem	ordtuni 20994*	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   &    |- A = ran ( x e. X |-> { y e. X | -. y R x } )   &    |- B = ran ( x e. X |-> { y e. X | -. x R y } )   =>    |- ( R e. V -> X = U. ( { X } u. ( A u. B ) ) )
Theorem	ordtbas2 20995*	Lemma for ordtbas 20996. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   &    |- A = ran ( x e. X |-> { y e. X | -. y R x } )   &    |- B = ran ( x e. X |-> { y e. X | -. x R y } )   &    |- C = ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } )   =>    |- ( R e. TosetRel -> ( fi ` ( A u. B ) ) = ( ( A u. B ) u. C ) )
Theorem	ordtbas 20996*	In a total order, the finite intersections of the open rays generates the set of open intervals, but no more - these four collections form a subbasis for the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   &    |- A = ran ( x e. X |-> { y e. X | -. y R x } )   &    |- B = ran ( x e. X |-> { y e. X | -. x R y } )   &    |- C = ran ( a e. X , b e. X |-> { y e. X | ( -. y R a /\ -. b R y ) } )   =>    |- ( R e. TosetRel -> ( fi ` ( { X } u. ( A u. B ) ) ) = ( ( { X } u. ( A u. B ) ) u. C ) )
Theorem	ordttopon 20997	Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   =>    |- ( R e. V -> (ordTop ` R ) e. (TopOn ` X ) )
Theorem	ordtopn1 20998*	An upward ray ( P , +oo ) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. V /\ P e. X ) -> { x e. X | -. x R P } e. (ordTop ` R ) )
Theorem	ordtopn2 20999*	A downward ray ( -oo , P ) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. V /\ P e. X ) -> { x e. X | -. P R x } e. (ordTop ` R ) )
Theorem	ordtopn3 21000*	An open interval ( A , B ) is open. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | ( -. x R A /\ -. B R x ) } e. (ordTop ` R ) )