P. 202 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 20101-20200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	perflp 20101	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 20102	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 20103	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 20104	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 20105	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 20106	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 20107	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 20108	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 20109	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 20110	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 20111	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 20112	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 20113	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 20114	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 20115	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 20116	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 20117	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 20118	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 20119*	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 20120	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 20121	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 20122	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 20123	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 20124	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 20125	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 20126	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 20127	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 20128	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 20129	An interior in a subspace topology. Willard in General Topology says that there is no analog of restcls 20128 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 20130	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 20131	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 20132	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 20133	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 20134	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 20135*	Lemma for ordtbas 20139. 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 20136*	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 20137*	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 20138*	Lemma for ordtbas 20139. (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 20139*	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 20140	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 20141*	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 20142*	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 20143*	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 ) )
Theorem	ordtcld1 20144*	A downward ray ( -oo , P ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. V /\ P e. X ) -> { x e. X | x R P } e. ( Clsd ` (ordTop ` R ) ) )
Theorem	ordtcld2 20145*	An upward ray [ P , +oo ) is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. V /\ P e. X ) -> { x e. X | P R x } e. ( Clsd ` (ordTop ` R ) ) )
Theorem	ordtcld3 20146*	A closed interval [ A , B ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- X = dom R   =>    |- ( ( R e. V /\ A e. X /\ B e. X ) -> { x e. X | ( A R x /\ x R B ) } e. ( Clsd ` (ordTop ` R ) ) )
Theorem	ordttop 20147	The order topology is a topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( R e. V -> (ordTop ` R ) e. Top )
Theorem	ordtcnv 20148	The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( R e. PosetRel -> (ordTop ` `' R ) = (ordTop ` R ) )
Theorem	ordtrest 20149	The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( ( R e. PosetRel /\ A e. V ) -> (ordTop ` ( R i^i ( A X. A ) ) ) C_ ( (ordTop ` R ) ↾t A ) )
Theorem	ordtrest2lem 20150*	Lemma for ordtrest2 20151. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   &    |- ( ph -> R e. TosetRel )   &    |- ( ph -> A C_ X )   &    |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } C_ A )   =>    |- ( ph -> A. v e. ran ( z e. X |-> { w e. X | -. w R z } ) ( v i^i A ) e. (ordTop ` ( R i^i ( A X. A ) ) ) )
Theorem	ordtrest2 20151*	An interval-closed set A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in RR, but in other sets like QQ there are interval-closed sets like ( pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.)
|- X = dom R   &    |- ( ph -> R e. TosetRel )   &    |- ( ph -> A C_ X )   &    |- ( ( ph /\ ( x e. A /\ y e. A ) ) -> { z e. X | ( x R z /\ z R y ) } C_ A )   =>    |- ( ph -> (ordTop ` ( R i^i ( A X. A ) ) ) = ( (ordTop ` R ) ↾t A ) )
Theorem	letopon 20152	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- (ordTop ` <_ ) e. (TopOn ` RR* )
Theorem	letop 20153	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- (ordTop ` <_ ) e. Top
Theorem	letopuni 20154	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- RR* = U. (ordTop ` <_ )
Theorem	xrstopn 20155	The topology component of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- (ordTop ` <_ ) = ( TopOpen ` RR*s )
Theorem	xrstps 20156	The extended real number structure is a topological space. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- RR*s e. TopSp
Theorem	leordtvallem1 20157*	Lemma for leordtval 20160. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )   =>    |- A = ran ( x e. RR* |-> { y e. RR* | -. y <_ x } )
Theorem	leordtvallem2 20158*	Lemma for leordtval 20160. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )   &    |- B = ran ( x e. RR* |-> ( -oo [,) x ) )   =>    |- B = ran ( x e. RR* |-> { y e. RR* | -. x <_ y } )
Theorem	leordtval2 20159	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )   &    |- B = ran ( x e. RR* |-> ( -oo [,) x ) )   =>    |- (ordTop ` <_ ) = ( topGen ` ( fi ` ( A u. B ) ) )
Theorem	leordtval 20160	The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- A = ran ( x e. RR* |-> ( x (,] +oo ) )   &    |- B = ran ( x e. RR* |-> ( -oo [,) x ) )   &    |- C = ran (,)   =>    |- (ordTop ` <_ ) = ( topGen ` ( ( A u. B ) u. C ) )
Theorem	iccordt 20161	A closed interval is closed in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A [,] B ) e. ( Clsd ` (ordTop ` <_ ) )
Theorem	iocpnfordt 20162	An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A (,] +oo ) e. (ordTop ` <_ )
Theorem	icomnfordt 20163	An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( -oo [,) A ) e. (ordTop ` <_ )
Theorem	iooordt 20164	An open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( A (,) B ) e. (ordTop ` <_ )
Theorem	reordt 20165	The real numbers are an open set in the topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- RR e. (ordTop ` <_ )
Theorem	lecldbas 20166	The set of closed intervals forms a closed subbasis for the topology on the extended reals. Since our definition of a basis is in terms of open sets, we express this by showing that the complements of closed intervals form an open subbasis for the topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- F = ( x e. ran [,] |-> ( RR* \ x ) )   =>    |- (ordTop ` <_ ) = ( topGen ` ( fi ` ran F ) )
Theorem	pnfnei 20167*	A neighborhood of +oo contains an unbounded interval based at a real number. Together with xrtgioo 21735 (which describes neighborhoods of RR) and mnfnei 20168, this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt 20164 and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. (ordTop ` <_ ) /\ +oo e. A ) -> E. x e. RR ( x (,] +oo ) C_ A )
Theorem	mnfnei 20168*	A neighborhood of -oo contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015.)
|- ( ( A e. (ordTop ` <_ ) /\ -oo e. A ) -> E. x e. RR ( -oo [,) x ) C_ A )
Theorem	ordtrestixx 20169*	The restriction of the less than order to an interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- A C_ RR*   &    |- ( ( x e. A /\ y e. A ) -> ( x [,] y ) C_ A )   =>    |- ( (ordTop ` <_ ) ↾t A ) = (ordTop ` ( <_ i^i ( A X. A ) ) )
Theorem	ordtresticc 20170	The restriction of the less than order to a closed interval gives the same topology as the subspace topology. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( (ordTop ` <_ ) ↾t ( A [,] B ) ) = (ordTop ` ( <_ i^i ( ( A [,] B ) X. ( A [,] B ) ) ) )
12.1.9  Limits and continuity in topological spaces
Syntax	ccn 20171	Extend class notation with the set of continuous functions between topologies.
class Cn
Syntax	ccnp 20172	Extend class notation with the set of functions between topologies continuous at a point.
class CnP
Syntax	clm 20173	Extend class notation with a function on topological spaces whose value is the convergence relation for limit sequences in the space.
class ~~> t
Definition	df-cn 20174*	Define a function on two topologies whose value is the set of continuous mappings from the first topology to the second. Based on definition of continuous function in [Munkres] p. 102. See iscn 20182 for the predicate form. (Contributed by NM, 17-Oct-2006.)
|- Cn = ( j e. Top , k e. Top |-> { f e. ( U. k ^m U. j ) | A. y e. k ( `' f " y ) e. j } )
Definition	df-cnp 20175*	Define a function on two topologies whose value is the set of continuous mappings at a specified point in the first topology. Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.)
|- CnP = ( j e. Top , k e. Top |-> ( x e. U. j |-> { f e. ( U. k ^m U. j ) | A. y e. k ( ( f ` x ) e. y -> E. g e. j ( x e. g /\ ( f " g ) C_ y ) ) } ) )
Definition	df-lm 20176*	Define a function on topologies whose value is the convergence relation for the space. Although f is typically a function from upper integers to the topological space, it doesn't have to be. Unfortunately, the value of the function must exist to use fvmpt 5964, and we use the otherwise unnecessary conjunct dom f C_ CC to ensure that. (Contributed by NM, 7-Sep-2006.)
|- ~~> t = ( j e. Top |-> { <. f , x >. | ( f e. ( U. j ^pm CC ) /\ x e. U. j /\ A. u e. j ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
Theorem	lmrel 20177	The topological space convergence relation is a relation. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- Rel ( ~~> t ` J )
Theorem	lmrcl 20178	Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.)
|- ( F ( ~~> t ` J ) P -> J e. Top )
Theorem	lmfval 20179*	The relation "sequence f converges to point y " in a metric space. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( J e. (TopOn ` X ) -> ( ~~> t ` J ) = { <. f , x >. | ( f e. ( X ^pm CC ) /\ x e. X /\ A. u e. J ( x e. u -> E. y e. ran ZZ>= ( f |` y ) : y --> u ) ) } )
Theorem	cnfval 20180*	The set of all continuous functions from topology J to topology K. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( J Cn K ) = { f e. ( Y ^m X ) | A. y e. K ( `' f " y ) e. J } )
Theorem	cnpfval 20181*	The function mapping the points in a topology J to the set of all functions from J to topology K continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( J CnP K ) = ( x e. X |-> { f e. ( Y ^m X ) | A. w e. K ( ( f ` x ) e. w -> E. v e. J ( x e. v /\ ( f " v ) C_ w ) ) } ) )
Theorem	iscn 20182*	The predicate " F is a continuous function from topology J to topology K." Definition of continuous function in [Munkres] p. 102. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
Theorem	cnpval 20183*	The set of all functions from topology J to topology K that are continuous at a point P. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( ( J CnP K ) ` P ) = { f e. ( Y ^m X ) | A. y e. K ( ( f ` P ) e. y -> E. x e. J ( P e. x /\ ( f " x ) C_ y ) ) } )
Theorem	iscnp 20184*	The predicate " F is a continuous function from topology J to topology K at point P." Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
Theorem	iscn2 20185*	The predicate " F is a continuous function from topology J to topology K." Definition of continuous function in [Munkres] p. 102. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( J Cn K ) <-> ( ( J e. Top /\ K e. Top ) /\ ( F : X --> Y /\ A. y e. K ( `' F " y ) e. J ) ) )
Theorem	iscnp2 20186*	The predicate " F is a continuous function from topology J to topology K at point P." Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( ( J CnP K ) ` P ) <-> ( ( J e. Top /\ K e. Top /\ P e. X ) /\ ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )
Theorem	cntop1 20187	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> J e. Top )
Theorem	cntop2 20188	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> K e. Top )
Theorem	cnptop1 20189	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( ( J CnP K ) ` P ) -> J e. Top )
Theorem	cnptop2 20190	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( ( J CnP K ) ` P ) -> K e. Top )
Theorem	iscnp3 20191*	The predicate " F is a continuous function from topology J to topology K at point P." (Contributed by NM, 15-May-2007.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. K ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ x C_ ( `' F " y ) ) ) ) ) )
Theorem	cnprcl 20192	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( F e. ( ( J CnP K ) ` P ) -> P e. X )
Theorem	cnf 20193	A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( J Cn K ) -> F : X --> Y )
Theorem	cnpf 20194	A continuous function at point P is a mapping. (Contributed by FL, 17-Nov-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( ( J CnP K ) ` P ) -> F : X --> Y )
Theorem	cnpcl 20195	The value of a continuous function from J to K at point P belongs to the underlying set of topology K. (Contributed by FL, 27-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( F e. ( ( J CnP K ) ` P ) /\ A e. X ) -> ( F ` A ) e. Y )
Theorem	cnf2 20196	A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( J Cn K ) ) -> F : X --> Y )
Theorem	cnpf2 20197	A continuous function at point P is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
Theorem	cnprcl2 20198	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ F e. ( ( J CnP K ) ` P ) ) -> P e. X )
Theorem	tgcn 20199*	The continuity predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K = ( topGen ` B ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )
Theorem	tgcnp 20200*	The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K = ( topGen ` B ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> P e. X )   =>    |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. B ( ( F ` P ) e. y -> E. x e. J ( P e. x /\ ( F " x ) C_ y ) ) ) ) )