P. 196 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19501-19600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscnp2 19501*	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 19502	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> J e. Top )
Theorem	cntop2 19503	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> K e. Top )
Theorem	cnptop1 19504	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 19505	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 19506*	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 19507	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 19508	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 19509	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 19510	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 19511	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 19512	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 19513	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 19514*	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 19515*	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 ) ) ) ) )
Theorem	subbascn 19516*	The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> B e. V )   &    |- ( ph -> K = ( topGen ` ( fi ` B ) ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. y e. B ( `' F " y ) e. J ) ) )
Theorem	ssidcn 19517	The identity function is a continuous function from one topology to another topology on the same set iff the domain is finer than the codomain. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) ) -> ( ( _I |` X ) e. ( J Cn K ) <-> K C_ J ) )
Theorem	cnpimaex 19518*	Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.)
|- ( ( F e. ( ( J CnP K ) ` P ) /\ A e. K /\ ( F ` P ) e. A ) -> E. x e. J ( P e. x /\ ( F " x ) C_ A ) )
Theorem	idcn 19519	A restricted identity function is a continuous function. (Contributed by FL, 27-Dec-2006.) (Proof shortened by Mario Carneiro, 21-Mar-2015.)
|- ( J e. (TopOn ` X ) -> ( _I |` X ) e. ( J Cn J ) )
Theorem	lmbr 19520*	Express the binary relation "sequence F converges to point P " in a topological space. Definition 1.4-1 of [Kreyszig] p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm 19491. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ph -> J e. (TopOn ` X ) )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. y e. ran ZZ>= ( F |` y ) : y --> u ) ) ) )
Theorem	lmbr2 19521*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
Theorem	lmbrf 19522*	Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. This version of lmbr2 19521 presupposes that F is a function. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> X )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) A e. u ) ) ) )
Theorem	lmconst 19523	A constant sequence converges to its value. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 14-Nov-2013.)
|- Z = ( ZZ>= ` M )   =>    |- ( ( J e. (TopOn ` X ) /\ P e. X /\ M e. ZZ ) -> ( Z X. { P } ) ( ~~> t ` J ) P )
Theorem	lmcvg 19524*	Convergence property of a converging sequence. (Contributed by Mario Carneiro, 14-Nov-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> P e. U )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> U e. J )   =>    |- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. U )
Theorem	iscnp4 19525*	The predicate " F is a continuous function from topology J to topology K at point P." in terms of neighborhoods. (Contributed by FL, 18-Jul-2011.) (Revised by Mario Carneiro, 10-Sep-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. y e. ( ( nei ` K ) ` { ( F ` P ) } ) E. x e. ( ( nei ` J ) ` { P } ) ( F " x ) C_ y ) ) )
Theorem	cnpnei 19526*	A condition for continuity at a point in terms of neighborhoods. (Contributed by Jeff Hankins, 7-Sep-2009.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top /\ F : X --> Y ) /\ A e. X ) -> ( F e. ( ( J CnP K ) ` A ) <-> A. y e. ( ( nei ` K ) ` { ( F ` A ) } ) ( `' F " y ) e. ( ( nei ` J ) ` { A } ) ) )
Theorem	cnima 19527	An open subset of the codomain of a continuous function has an open preimage. (Contributed by FL, 15-Dec-2006.)
|- ( ( F e. ( J Cn K ) /\ A e. K ) -> ( `' F " A ) e. J )
Theorem	cnco 19528	The composition of two continuous functions is a continuous function. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( F e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( G o. F ) e. ( J Cn L ) )
Theorem	cnpco 19529	The composition of two continuous functions at point P is a continuous function at point P. Proposition of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
|- ( ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) -> ( G o. F ) e. ( ( J CnP L ) ` P ) )
Theorem	cnclima 19530	A closed subset of the codomain of a continuous function has a closed preimage. (Contributed by NM, 15-Mar-2007.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( F e. ( J Cn K ) /\ A e. ( Clsd ` K ) ) -> ( `' F " A ) e. ( Clsd ` J ) )
Theorem	iscncl 19531*	A definition of a continuous function using closed sets. Theorem 1 (d) of [BourbakiTop1] p. I.9. (Contributed by FL, 19-Nov-2006.) (Proof shortened 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. ( Clsd ` K ) ( `' F " y ) e. ( Clsd ` J ) ) ) )
Theorem	cncls2i 19532	Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- Y = U. K   =>    |- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( ( cls ` J ) ` ( `' F " S ) ) C_ ( `' F " ( ( cls ` K ) ` S ) ) )
Theorem	cnntri 19533	Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- Y = U. K   =>    |- ( ( F e. ( J Cn K ) /\ S C_ Y ) -> ( `' F " ( ( int ` K ) ` S ) ) C_ ( ( int ` J ) ` ( `' F " S ) ) )
Theorem	cnclsi 19534	Property of the image of a closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Cn K ) /\ S C_ X ) -> ( F " ( ( cls ` J ) ` S ) ) C_ ( ( cls ` K ) ` ( F " S ) ) )
Theorem	cncls2 19535*	Continuity in terms of closure. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P Y ( ( cls ` J ) ` ( `' F " x ) ) C_ ( `' F " ( ( cls ` K ) ` x ) ) ) ) )
Theorem	cncls 19536*	Continuity in terms of closure. (Contributed by Jeff Hankins, 1-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P X ( F " ( ( cls ` J ) ` x ) ) C_ ( ( cls ` K ) ` ( F " x ) ) ) ) )
Theorem	cnntr 19537*	Continuity in terms of interior. (Contributed by Jeff Hankins, 2-Oct-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. ~P Y ( `' F " ( ( int ` K ) ` x ) ) C_ ( ( int ` J ) ` ( `' F " x ) ) ) ) )
Theorem	cnss1 19538	If the topology K is finer than J, then there are more continuous functions from K than from J. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( ( K e. (TopOn ` X ) /\ J C_ K ) -> ( J Cn L ) C_ ( K Cn L ) )
Theorem	cnss2 19539	If the topology K is finer than J, then there are fewer continuous functions into K than into J from some other space. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- Y = U. K   =>    |- ( ( L e. (TopOn ` Y ) /\ L C_ K ) -> ( J Cn K ) C_ ( J Cn L ) )
Theorem	cncnpi 19540	A continuous function is continuous at all points. One direction of Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Cn K ) /\ A e. X ) -> F e. ( ( J CnP K ) ` A ) )
Theorem	cnsscnp 19541	The set of continuous functions is a subset of the set of continuous functions at a point. (Contributed by Raph Levien, 21-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( P e. X -> ( J Cn K ) C_ ( ( J CnP K ) ` P ) )
Theorem	cncnp 19542*	A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by NM, 15-May-2007.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
Theorem	cncnp2 19543*	A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( X =/= (/) -> ( F e. ( J Cn K ) <-> A. x e. X F e. ( ( J CnP K ) ` x ) ) )
Theorem	cnnei 19544*	Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( J e. Top /\ K e. Top /\ F : X --> Y ) -> ( F e. ( J Cn K ) <-> A. p e. X A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )
Theorem	cnconst2 19545	A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ B e. Y ) -> ( X X. { B } ) e. ( J Cn K ) )
Theorem	cnconst 19546	A constant function is continuous. (Contributed by FL, 15-Jan-2007.) (Proof shortened by Mario Carneiro, 19-Mar-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) /\ ( B e. Y /\ F : X --> { B } ) ) -> F e. ( J Cn K ) )
Theorem	cnrest 19547	Continuity of a restriction from a subspace. (Contributed by Jeff Hankins, 11-Jul-2009.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Cn K ) /\ A C_ X ) -> ( F |` A ) e. ( ( J ↾t A ) Cn K ) )
Theorem	cnrest2 19548	Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Hankins, 10-Jul-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- ( ( K e. (TopOn ` Y ) /\ ran F C_ B /\ B C_ Y ) -> ( F e. ( J Cn K ) <-> F e. ( J Cn ( K ↾t B ) ) ) )
Theorem	cnrest2r 19549	Equivalence of continuity in the parent topology and continuity in a subspace. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.)
|- ( K e. Top -> ( J Cn ( K ↾t B ) ) C_ ( J Cn K ) )
Theorem	cnpresti 19550	One direction of cnprest 19551 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 1-May-2015.)
|- X = U. J   =>    |- ( ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) -> ( F |` A ) e. ( ( ( J ↾t A ) CnP K ) ` P ) )
Theorem	cnprest 19551	Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ A C_ X ) /\ ( P e. ( ( int ` J ) ` A ) /\ F : X --> Y ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F |` A ) e. ( ( ( J ↾t A ) CnP K ) ` P ) ) )
Theorem	cnprest2 19552	Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( K e. Top /\ F : X --> B /\ B C_ Y ) -> ( F e. ( ( J CnP K ) ` P ) <-> F e. ( ( J CnP ( K ↾t B ) ) ` P ) ) )
Theorem	cndis 19553	Every function is continuous when the domain is discrete. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( ~P A Cn J ) = ( X ^m A ) )
Theorem	cnindis 19554	Every function is continuous when the codomain is indiscrete (trivial). (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 21-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ A e. V ) -> ( J Cn { (/) , A } ) = ( A ^m X ) )
Theorem	cnpdis 19555	If A is an isolated point in X (or equivalently, the singleton { A } is open in X), then every function is continuous at A. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ A e. X ) /\ { A } e. J ) -> ( ( J CnP K ) ` A ) = ( Y ^m X ) )
Theorem	paste 19556	Pasting lemma. If A and B are closed sets in X with A u. B = X, then any function whose restrictions to A and B are continuous is continuous on all of X. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 21-Aug-2015.)
|- X = U. J   &    |- Y = U. K   &    |- ( ph -> A e. ( Clsd ` J ) )   &    |- ( ph -> B e. ( Clsd ` J ) )   &    |- ( ph -> ( A u. B ) = X )   &    |- ( ph -> F : X --> Y )   &    |- ( ph -> ( F |` A ) e. ( ( J ↾t A ) Cn K ) )   &    |- ( ph -> ( F |` B ) e. ( ( J ↾t B ) Cn K ) )   =>    |- ( ph -> F e. ( J Cn K ) )
Theorem	lmfpm 19557	If F converges, then F is a partial function. (Contributed by Mario Carneiro, 23-Dec-2013.)
|- ( ( J e. (TopOn ` X ) /\ F ( ~~> t ` J ) P ) -> F e. ( X ^pm CC ) )
Theorem	lmfss 19558	Inclusion of a function having a limit (used to ensure the limit relation is a set, under our definition). (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- ( ( J e. (TopOn ` X ) /\ F ( ~~> t ` J ) P ) -> F C_ ( CC X. X ) )
Theorem	lmcl 19559	Closure of a limit. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- ( ( J e. (TopOn ` X ) /\ F ( ~~> t ` J ) P ) -> P e. X )
Theorem	lmss 19560	Limit on a subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
|- K = ( J ↾t Y )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> Y e. V )   &    |- ( ph -> J e. Top )   &    |- ( ph -> P e. Y )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F : Z --> Y )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> F ( ~~> t ` K ) P ) )
Theorem	sslm 19561	A finer topology has fewer convergent sequences (but the sequences that do converge, converge to the same value). (Contributed by Mario Carneiro, 15-Sep-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` X ) /\ J C_ K ) -> ( ~~> t ` K ) C_ ( ~~> t ` J ) )
Theorem	lmres 19562	A function converges iff its restriction to an upper integers set converges. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> F e. ( X ^pm CC ) )   &    |- ( ph -> M e. ZZ )   =>    |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F |` ( ZZ>= ` M ) ) ( ~~> t ` J ) P ) )
Theorem	lmff 19563*	If F converges, there is some upper integer set on which F is a total function. (Contributed by Mario Carneiro, 31-Dec-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F e. dom ( ~~> t ` J ) )   =>    |- ( ph -> E. j e. Z ( F |` ( ZZ>= ` j ) ) : ( ZZ>= ` j ) --> X )
Theorem	lmcls 19564*	Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013.) (Revised by Mario Carneiro, 1-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. S )   &    |- ( ph -> S C_ X )   =>    |- ( ph -> P e. ( ( cls ` J ) ` S ) )
Theorem	lmcld 19565*	Any convergent sequence of points in a closed subset of a topological space converges to a point in the set. (Contributed by Mario Carneiro, 30-Dec-2013.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. S )   &    |- ( ph -> S e. ( Clsd ` J ) )   =>    |- ( ph -> P e. S )
Theorem	lmcnp 19566	The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)
|- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> G e. ( ( J CnP K ) ` P ) )   =>    |- ( ph -> ( G o. F ) ( ~~> t ` K ) ( G ` P ) )
Theorem	lmcn 19567	The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)
|- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> G e. ( J Cn K ) )   =>    |- ( ph -> ( G o. F ) ( ~~> t ` K ) ( G ` P ) )
12.1.10  Separated spaces: T0, T1, T2 (Hausdorff) ...
Syntax	ct0 19568	Extend class notation with the class of all T0 spaces.
class Kol2
Syntax	ct1 19569	Extend class notation to include T1 spaces (also called Fréchet spaces).
class Fre
Syntax	cha 19570	Extend class notation with the class of all Hausdorff spaces.
class Haus
Syntax	creg 19571	Extend class notation with the class of all regular topologies.
class Reg
Syntax	cnrm 19572	Extend class notation with the class of all normal topologies.
class Nrm
Syntax	ccnrm 19573	Extend class notation with the class of all completely normal topologies.
class CNrm
Syntax	cpnrm 19574	Extend class notation with the class of all perfectly normal topologies.
class PNrm
Definition	df-t0 19575*	Define T0 or Kolmogorov spaces. A T0 space satisfies a kind of "topological extensionality" principle (compare ax-ext 2440): any two points which are members of the same open sets are equal, or in contraposition, for any two distinct points there is an open set which contains one point but not the other. This differs from T1 spaces (see ist1-2 19609) in that in a T1 space you can choose which point will be in the open set and which outside; in a T0 space you only know that one of the two points is in the set. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- Kol2 = { j e. Top | A. x e. U. j A. y e. U. j ( A. o e. j ( x e. o <-> y e. o ) -> x = y ) }
Definition	df-t1 19576*	The class of all T1 spaces, also called Fréchet spaces. Morris, Topology without tears, p. 30 ex. 3. (Contributed by FL, 18-Jun-2007.)
|- Fre = { x e. Top | A. a e. U. x { a } e. ( Clsd ` x ) }
Definition	df-haus 19577*	Define the class of all Hausdorff spaces. A Hausdorff space is a topology in which distinct points have disjoint open neighborhoods. Definition of Hausdorff space in [Munkres] p. 98. (Contributed by NM, 8-Mar-2007.)
|- Haus = { j e. Top | A. x e. U. j A. y e. U. j ( x =/= y -> E. n e. j E. m e. j ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) }
Definition	df-reg 19578*	Define regular spaces. A space is regular if a point and a closed set can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) }
Definition	df-nrm 19579*	Define normal spaces. A space is normal if disjoint closed sets can be separated by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- Nrm = { j e. Top | A. x e. j A. y e. ( ( Clsd ` j ) i^i ~P x ) E. z e. j ( y C_ z /\ ( ( cls ` j ) ` z ) C_ x ) }
Definition	df-cnrm 19580*	Define completely normal spaces. A space is completely normal if all its subspaces are normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- CNrm = { j e. Top | A. x e. ~P U. j ( j ↾t x ) e. Nrm }
Definition	df-pnrm 19581*	Define perfectly normal spaces. A space is perfectly normal if it is normal and every closed set is a G&delta; set, meaning that it is a countable intersection of open sets. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- PNrm = { j e. Nrm | ( Clsd ` j ) C_ ran ( f e. ( j ^m NN ) |-> |^| ran f ) }
Theorem	ist0 19582*	The predicate "is a T0 space." Every pair of distinct points is topologically distinguishable. For the way this definition is usually encountered, see ist0-3 19607. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- X = U. J   =>    |- ( J e. Kol2 <-> ( J e. Top /\ A. x e. X A. y e. X ( A. o e. J ( x e. o <-> y e. o ) -> x = y ) ) )
Theorem	ist1 19583*	The predicate J is T1. (Contributed by FL, 18-Jun-2007.)
|- X = U. J   =>    |- ( J e. Fre <-> ( J e. Top /\ A. a e. X { a } e. ( Clsd ` J ) ) )
Theorem	ishaus 19584*	Express the predicate " J is a Hausdorff space." (Contributed by NM, 8-Mar-2007.)
|- X = U. J   =>    |- ( J e. Haus <-> ( J e. Top /\ A. x e. X A. y e. X ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) )
Theorem	iscnrm 19585*	The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- X = U. J   =>    |- ( J e. CNrm <-> ( J e. Top /\ A. x e. ~P X ( J ↾t x ) e. Nrm ) )
Theorem	t0sep 19586*	Any two topologically indistinguishable points in a T0 space are identical. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( J e. Kol2 /\ ( A e. X /\ B e. X ) ) -> ( A. x e. J ( A e. x <-> B e. x ) -> A = B ) )
Theorem	t0dist 19587*	Any two distinct points in a T0 space are topologically distinguishable. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- X = U. J   =>    |- ( ( J e. Kol2 /\ ( A e. X /\ B e. X /\ A =/= B ) ) -> E. o e. J -. ( A e. o <-> B e. o ) )
Theorem	t1sncld 19588	In a T1 space, one-point sets are closed. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- X = U. J   =>    |- ( ( J e. Fre /\ A e. X ) -> { A } e. ( Clsd ` J ) )
Theorem	t1ficld 19589	In a T1 space, finite sets are closed. (Contributed by Mario Carneiro, 25-Dec-2016.)
|- X = U. J   =>    |- ( ( J e. Fre /\ A C_ X /\ A e. Fin ) -> A e. ( Clsd ` J ) )
Theorem	hausnei 19590*	Neighborhood property of a Hausdorff space. (Contributed by NM, 8-Mar-2007.)
|- X = U. J   =>    |- ( ( J e. Haus /\ ( P e. X /\ Q e. X /\ P =/= Q ) ) -> E. n e. J E. m e. J ( P e. n /\ Q e. m /\ ( n i^i m ) = (/) ) )
Theorem	t0top 19591	A T0 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- ( J e. Kol2 -> J e. Top )
Theorem	t1top 19592	A T1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- ( J e. Fre -> J e. Top )
Theorem	haustop 19593	A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007.)
|- ( J e. Haus -> J e. Top )
Theorem	isreg 19594*	The predicate "is a regular space." In a regular space, any open neighborhood has a closed subneighborhood. Note that some authors require the space to be Hausdorff (which would make it the same as T3), but we reserve the phrase "regular Hausdorff" for that as many topologists do. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 25-Aug-2015.)
|- ( J e. Reg <-> ( J e. Top /\ A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
Theorem	regtop 19595	A regular space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- ( J e. Reg -> J e. Top )
Theorem	regsep 19596*	In a regular space, every neighborhood of a point contains a closed subneighborhood. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- ( ( J e. Reg /\ U e. J /\ A e. U ) -> E. x e. J ( A e. x /\ ( ( cls ` J ) ` x ) C_ U ) )
Theorem	isnrm 19597*	The predicate "is a normal space." Much like the case for regular spaces, normal does not imply Hausdorff or even regular. (Contributed by Jeff Hankins, 1-Feb-2010.) (Revised by Mario Carneiro, 24-Aug-2015.)
|- ( J e. Nrm <-> ( J e. Top /\ A. x e. J A. y e. ( ( Clsd ` J ) i^i ~P x ) E. z e. J ( y C_ z /\ ( ( cls ` J ) ` z ) C_ x ) ) )
Theorem	nrmtop 19598	A normal space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010.)
|- ( J e. Nrm -> J e. Top )
Theorem	cnrmtop 19599	A completely normal space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( J e. CNrm -> J e. Top )
Theorem	iscnrm2 19600*	The property of being completely or hereditarily normal. (Contributed by Mario Carneiro, 26-Aug-2015.)
|- ( J e. (TopOn ` X ) -> ( J e. CNrm <-> A. x e. ~P X ( J ↾t x ) e. Nrm ) )