P. 149 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14801-14900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cls0 14801	The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.)
|- ( J e. Top -> ( ( cls ` J ) ` (/) ) = (/) )
Theorem	ntr0 14802	The interior of the empty set. (Contributed by NM, 2-Oct-2007.)
|- ( J e. Top -> ( ( int ` J ) ` (/) ) = (/) )
Theorem	isopn3i 14803	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	discld 14804	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 14805	The closed sets of the topology { (/) }. (Contributed by FL, 5-Jan-2009.)
|- ( Clsd ` { (/) } ) = { (/) }
9.1.5  Neighborhoods
Syntax	cnei 14806	Extend class notation with neighborhood relation for topologies.
class nei
Definition	df-nei 14807*	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 14808*	Value of the neighborhood function on the subsets 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 -> ( nei ` J ) = ( x e. ~P X |-> { v e. ~P X | E. g e. J ( x C_ g /\ g C_ v ) } ) )
Theorem	neif 14809	The neighborhood function is a function from the set of the subsets of the base set of a topology. (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 14810	A set with a neighborhood is a subset of the base set of a topology. (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 14811*	Value of 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 14812*	The predicate "the class 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 14813	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 14814*	The predicate "the class 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 14815	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 14816	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 14817*	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 14818	Any neighborhood of a set S is also a neighborhood of any subset R C_ S. Similar to Proposition 1 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 14819	A set is included in any of its neighborhoods. Generalization to subsets of elnei 14820. (Contributed by FL, 16-Nov-2006.)
|- ( ( J e. Top /\ N e. ( ( nei ` J ) ` S ) ) -> S C_ N )
Theorem	elnei 14820	A point belongs to any of its neighborhoods. Property 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 14821	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	neipsm 14822*	A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) (Revised by Jim Kingdon, 22-Mar-2023.)
|- X = U. J   =>    |- ( ( J e. Top /\ S C_ X /\ E. x x e. S ) -> ( N e. ( ( nei ` J ) ` S ) <-> A. p e. S N e. ( ( nei ` J ) ` { p } ) ) )
Theorem	opnneissb 14823	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 14824	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 14825	Any subset M of X containing a neighborhood N of a set S is a neighborhood of this set. Generalization to subsets of Property 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	opnneiss 14826	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 14827	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	tpnei 14828	The underlying set of a topology is a neighborhood of any of its subsets. Special case of opnneiss 14826. (Contributed by FL, 2-Oct-2006.)
|- X = U. J   =>    |- ( J e. Top -> ( S C_ X <-> X e. ( ( nei ` J ) ` S ) ) )
Theorem	neiuni 14829	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	topssnei 14830	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 14831	The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property Vii of [BourbakiTop1] p. I.3 for binary intersections. (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 14832	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 14833*	For any neighborhood N of S, there is a neighborhood x of S such that N is a neighborhood of all subsets of x. Generalization to subsets of Property 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 14834	The empty set is a neighborhood of itself. (Contributed by FL, 10-Dec-2006.)
|- ( J e. Top -> (/) e. ( ( nei ` J ) ` (/) ) )
9.1.6  Subspace topologies
Theorem	restrcl 14835	Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon, 23-Mar-2023.)
|- ( ( J ↾t A ) e. Top -> ( J e. _V /\ A e. _V ) )
Theorem	restbasg 14836	A subspace topology basis is a basis. (Contributed by Mario Carneiro, 19-Mar-2015.)
|- ( ( B e. TopBases /\ A e. V ) -> ( B ↾t A ) e. TopBases )
Theorem	tgrest 14837	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 14838	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 14839	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 14840	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 14841	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 14842	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 14843	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 14844	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 14845	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 14846	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 14847	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 14848	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	restopnb 14849	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 14850	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 14851	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 14852	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 )
9.1.7  Limits and continuity in topological spaces
Syntax	ccn 14853	Extend class notation with the class of continuous functions between topologies.
class Cn
Syntax	ccnp 14854	Extend class notation with the class of functions between topologies continuous at a given point.
class CnP
Syntax	clm 14855	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 14856*	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 14865 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 14857*	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 14858*	Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although f is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function ( x e. RR |-> ( sin ` ( pi x. x ) ) ) converges to zero (in the standard topology on the reals) with this definition. (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	lmrcl 14859	Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015.)
|- ( F ( ~~> t ` J ) P -> J e. Top )
Theorem	lmfval 14860*	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	lmreltop 14861	The topological space convergence relation is a relation. (Contributed by Jim Kingdon, 25-Mar-2023.)
|- ( J e. Top -> Rel ( ~~> t ` J ) )
Theorem	cnfval 14862*	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 14863*	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	cnovex 14864	The class of all continuous functions from a topology to another is a set. (Contributed by Jim Kingdon, 14-Dec-2023.)
|- ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V )
Theorem	iscn 14865*	The predicate "the class 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 14866*	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 14867*	The predicate "the class 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 14868*	The predicate "the class 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	cntop1 14869	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> J e. Top )
Theorem	cntop2 14870	Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( F e. ( J Cn K ) -> K e. Top )
Theorem	iscnp3 14871*	The predicate "the class 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	cnf 14872	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	cnf2 14873	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	cnprcl2k 14874	Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|- ( ( J e. (TopOn ` X ) /\ K e. Top /\ F e. ( ( J CnP K ) ` P ) ) -> P e. X )
Theorem	cnpf2 14875	A continuous function at point P is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
Theorem	tgcn 14876*	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 14877*	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	ssidcn 14878	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	icnpimaex 14879*	Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ P e. X ) /\ ( 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 14880	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 14881*	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 14858. (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 14882*	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 14883*	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 14882 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 14884	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 14885*	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 14886*	The predicate "the class 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 14887*	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 14888	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 14889	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	cnptopco 14890	The composition of a function F continuous at P with a function continuous at ( F ` P ) is continuous at P. Proposition 2 of [BourbakiTop1] p. I.9. (Contributed by FL, 16-Nov-2006.) (Proof shortened by Mario Carneiro, 27-Dec-2014.)
|- ( ( ( J e. Top /\ K e. Top /\ L e. Top ) /\ ( F e. ( ( J CnP K ) ` P ) /\ G e. ( ( K CnP L ) ` ( F ` P ) ) ) ) -> ( G o. F ) e. ( ( J CnP L ) ` P ) )
Theorem	cnclima 14891	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	cnntri 14892	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	cnntr 14893*	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 14894	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 14895	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 14896	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 14897	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 14898*	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	cncnp2m 14899*	A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Jim Kingdon, 30-Mar-2023.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( J e. Top /\ K e. Top /\ E. y y e. X ) -> ( F e. ( J Cn K ) <-> A. x e. X F e. ( ( J CnP K ) ` x ) ) )
Theorem	cnnei 14900*	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 ) )