P. 145 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14401-14500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnconst2 14401	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 14402	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 14403	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 14404	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 14405	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	cnptopresti 14406	One direction of cnptoprest 14407 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 Jim Kingdon, 31-Mar-2023.)
|- ( ( ( J e. (TopOn ` X ) /\ K e. Top ) /\ ( A C_ X /\ P e. A /\ F e. ( ( J CnP K ) ` P ) ) ) -> ( F |` A ) e. ( ( ( J ↾t A ) CnP K ) ` P ) )
Theorem	cnptoprest 14407	Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 5-Apr-2023.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K 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	cnptoprest2 14408	Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 6-Apr-2023.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ 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 14409	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	cnpdis 14410	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	lmfpm 14411	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 14412	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 14413	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 14414	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 14415	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 14416	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 14417*	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	lmtopcnp 14418	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.) (Revised by Jim Kingdon, 6-Apr-2023.)
|- ( ph -> F ( ~~> t ` J ) P )   &    |- ( ph -> K e. Top )   &    |- ( ph -> G e. ( ( J CnP K ) ` P ) )   =>    |- ( ph -> ( G o. F ) ( ~~> t ` K ) ( G ` P ) )
Theorem	lmcn 14419	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 ) )
9.1.8  Product topologies
Syntax	ctx 14420	Extend class notation with the binary topological product operation.
class tX
Definition	df-tx 14421*	Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- tX = ( r e. _V , s e. _V |-> ( topGen ` ran ( x e. r , y e. s |-> ( x X. y ) ) ) )
Theorem	txvalex 14422	Existence of the binary topological product. If R and S are known to be topologies, see txtop 14428. (Contributed by Jim Kingdon, 3-Aug-2023.)
|- ( ( R e. V /\ S e. W ) -> ( R tX S ) e. _V )
Theorem	txval 14423*	Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. V /\ S e. W ) -> ( R tX S ) = ( topGen ` B ) )
Theorem	txuni2 14424*	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   &    |- X = U. R   &    |- Y = U. S   =>    |- ( X X. Y ) = U. B
Theorem	txbasex 14425*	The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. V /\ S e. W ) -> B e. _V )
Theorem	txbas 14426*	The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 31-Aug-2015.)
|- B = ran ( x e. R , y e. S |-> ( x X. y ) )   =>    |- ( ( R e. TopBases /\ S e. TopBases ) -> B e. TopBases )
Theorem	eltx 14427*	A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( ( J e. V /\ K e. W ) -> ( S e. ( J tX K ) <-> A. p e. S E. x e. J E. y e. K ( p e. ( x X. y ) /\ ( x X. y ) C_ S ) ) )
Theorem	txtop 14428	The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
Theorem	txtopi 14429	The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- R e. Top   &    |- S e. Top   =>    |- ( R tX S ) e. Top
Theorem	txtopon 14430	The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( R tX S ) e. (TopOn ` ( X X. Y ) ) )
Theorem	txuni 14431	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- X = U. R   &    |- Y = U. S   =>    |- ( ( R e. Top /\ S e. Top ) -> ( X X. Y ) = U. ( R tX S ) )
Theorem	txunii 14432	The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.)
|- R e. Top   &    |- S e. Top   &    |- X = U. R   &    |- Y = U. S   =>    |- ( X X. Y ) = U. ( R tX S )
Theorem	txopn 14433	The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( ( R e. V /\ S e. W ) /\ ( A e. R /\ B e. S ) ) -> ( A X. B ) e. ( R tX S ) )
Theorem	txss12 14434	Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- ( ( ( B e. V /\ D e. W ) /\ ( A C_ B /\ C C_ D ) ) -> ( A tX C ) C_ ( B tX D ) )
Theorem	txbasval 14435	It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014.)
|- ( ( R e. V /\ S e. W ) -> ( ( topGen ` R ) tX ( topGen ` S ) ) = ( R tX S ) )
Theorem	neitx 14436	The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.)
|- X = U. J   &    |- Y = U. K   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( A e. ( ( nei ` J ) ` C ) /\ B e. ( ( nei ` K ) ` D ) ) ) -> ( A X. B ) e. ( ( nei ` ( J tX K ) ) ` ( C X. D ) ) )
Theorem	tx1cn 14437	Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( 1st |` ( X X. Y ) ) e. ( ( R tX S ) Cn R ) )
Theorem	tx2cn 14438	Continuity of the second projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- ( ( R e. (TopOn ` X ) /\ S e. (TopOn ` Y ) ) -> ( 2nd |` ( X X. Y ) ) e. ( ( R tX S ) Cn S ) )
Theorem	txcnp 14439*	If two functions are continuous at D, then the ordered pair of them is continuous at D into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> D e. X )   &    |- ( ph -> ( x e. X |-> A ) e. ( ( J CnP K ) ` D ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( ( J CnP L ) ` D ) )   =>    |- ( ph -> ( x e. X |-> <. A , B >. ) e. ( ( J CnP ( K tX L ) ) ` D ) )
Theorem	upxp 14440*	Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- P = ( 1st |` ( B X. C ) )   &    |- Q = ( 2nd |` ( B X. C ) )   =>    |- ( ( A e. D /\ F : A --> B /\ G : A --> C ) -> E! h ( h : A --> ( B X. C ) /\ F = ( P o. h ) /\ G = ( Q o. h ) ) )
Theorem	txcnmpt 14441*	A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- W = U. U   &    |- H = ( x e. W |-> <. ( F ` x ) , ( G ` x ) >. )   =>    |- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> H e. ( U Cn ( R tX S ) ) )
Theorem	uptx 14442*	Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- T = ( R tX S )   &    |- X = U. R   &    |- Y = U. S   &    |- Z = ( X X. Y )   &    |- P = ( 1st |` Z )   &    |- Q = ( 2nd |` Z )   =>    |- ( ( F e. ( U Cn R ) /\ G e. ( U Cn S ) ) -> E! h e. ( U Cn T ) ( F = ( P o. h ) /\ G = ( Q o. h ) ) )
Theorem	txcn 14443	A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- X = U. R   &    |- Y = U. S   &    |- Z = ( X X. Y )   &    |- W = U. U   &    |- P = ( 1st |` Z )   &    |- Q = ( 2nd |` Z )   =>    |- ( ( R e. Top /\ S e. Top /\ F : W --> Z ) -> ( F e. ( U Cn ( R tX S ) ) <-> ( ( P o. F ) e. ( U Cn R ) /\ ( Q o. F ) e. ( U Cn S ) ) ) )
Theorem	txrest 14444	The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Sep-2015.)
|- ( ( ( R e. V /\ S e. W ) /\ ( A e. X /\ B e. Y ) ) -> ( ( R tX S ) ↾t ( A X. B ) ) = ( ( R ↾t A ) tX ( S ↾t B ) ) )
Theorem	txdis 14445	The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( ( A e. V /\ B e. W ) -> ( ~P A tX ~P B ) = ~P ( A X. B ) )
Theorem	txdis1cn 14446*	A function is jointly continuous on a discrete left topology iff it is continuous as a function of its right argument, for each fixed left value. (Contributed by Mario Carneiro, 19-Sep-2015.)
|- ( ph -> X e. V )   &    |- ( ph -> J e. (TopOn ` Y ) )   &    |- ( ph -> K e. Top )   &    |- ( ph -> F Fn ( X X. Y ) )   &    |- ( ( ph /\ x e. X ) -> ( y e. Y |-> ( x F y ) ) e. ( J Cn K ) )   =>    |- ( ph -> F e. ( ( ~P X tX J ) Cn K ) )
Theorem	txlm 14447*	Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> F : Z --> X )   &    |- ( ph -> G : Z --> Y )   &    |- H = ( n e. Z |-> <. ( F ` n ) , ( G ` n ) >. )   =>    |- ( ph -> ( ( F ( ~~> t ` J ) R /\ G ( ~~> t ` K ) S ) <-> H ( ~~> t ` ( J tX K ) ) <. R , S >. ) )
Theorem	lmcn2 14448*	The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 15-May-2014.)
|- Z = ( ZZ>= ` M )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> F : Z --> X )   &    |- ( ph -> G : Z --> Y )   &    |- ( ph -> F ( ~~> t ` J ) R )   &    |- ( ph -> G ( ~~> t ` K ) S )   &    |- ( ph -> O e. ( ( J tX K ) Cn N ) )   &    |- H = ( n e. Z |-> ( ( F ` n ) O ( G ` n ) ) )   =>    |- ( ph -> H ( ~~> t ` N ) ( R O S ) )
9.1.9  Continuous function-builders
Theorem	cnmptid 14449*	The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   =>    |- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )
Theorem	cnmptc 14450*	A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> P e. Y )   =>    |- ( ph -> ( x e. X |-> P ) e. ( J Cn K ) )
Theorem	cnmpt11 14451*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( y e. Y |-> B ) e. ( K Cn L ) )   &    |- ( y = A -> B = C )   =>    |- ( ph -> ( x e. X |-> C ) e. ( J Cn L ) )
Theorem	cnmpt11f 14452*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> F e. ( K Cn L ) )   =>    |- ( ph -> ( x e. X |-> ( F ` A ) ) e. ( J Cn L ) )
Theorem	cnmpt1t 14453*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )   =>    |- ( ph -> ( x e. X |-> <. A , B >. ) e. ( J Cn ( K tX L ) ) )
Theorem	cnmpt12f 14454*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )   &    |- ( ph -> F e. ( ( K tX L ) Cn M ) )   =>    |- ( ph -> ( x e. X |-> ( A F B ) ) e. ( J Cn M ) )
Theorem	cnmpt12 14455*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn K ) )   &    |- ( ph -> ( x e. X |-> B ) e. ( J Cn L ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> ( y e. Y , z e. Z |-> C ) e. ( ( K tX L ) Cn M ) )   &    |- ( ( y = A /\ z = B ) -> C = D )   =>    |- ( ph -> ( x e. X |-> D ) e. ( J Cn M ) )
Theorem	cnmpt1st 14456*	The projection onto the first coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> x ) e. ( ( J tX K ) Cn J ) )
Theorem	cnmpt2nd 14457*	The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> y ) e. ( ( J tX K ) Cn K ) )
Theorem	cnmpt2c 14458*	A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> P e. Z )   =>    |- ( ph -> ( x e. X , y e. Y |-> P ) e. ( ( J tX K ) Cn L ) )
Theorem	cnmpt21 14459*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> ( z e. Z |-> B ) e. ( L Cn M ) )   &    |- ( z = A -> B = C )   =>    |- ( ph -> ( x e. X , y e. Y |-> C ) e. ( ( J tX K ) Cn M ) )
Theorem	cnmpt21f 14460*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> F e. ( L Cn M ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> ( F ` A ) ) e. ( ( J tX K ) Cn M ) )
Theorem	cnmpt2t 14461*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> <. A , B >. ) e. ( ( J tX K ) Cn ( L tX M ) ) )
Theorem	cnmpt22 14462*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )   &    |- ( ph -> L e. (TopOn ` Z ) )   &    |- ( ph -> M e. (TopOn ` W ) )   &    |- ( ph -> ( z e. Z , w e. W |-> C ) e. ( ( L tX M ) Cn N ) )   &    |- ( ( z = A /\ w = B ) -> C = D )   =>    |- ( ph -> ( x e. X , y e. Y |-> D ) e. ( ( J tX K ) Cn N ) )
Theorem	cnmpt22f 14463*	The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   &    |- ( ph -> ( x e. X , y e. Y |-> B ) e. ( ( J tX K ) Cn M ) )   &    |- ( ph -> F e. ( ( L tX M ) Cn N ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> ( A F B ) ) e. ( ( J tX K ) Cn N ) )
Theorem	cnmpt1res 14464*	The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.)
|- K = ( J ↾t Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> ( x e. X |-> A ) e. ( J Cn L ) )   =>    |- ( ph -> ( x e. Y |-> A ) e. ( K Cn L ) )
Theorem	cnmpt2res 14465*	The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- K = ( J ↾t Y )   &    |- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> Y C_ X )   &    |- N = ( M ↾t W )   &    |- ( ph -> M e. (TopOn ` Z ) )   &    |- ( ph -> W C_ Z )   &    |- ( ph -> ( x e. X , y e. Z |-> A ) e. ( ( J tX M ) Cn L ) )   =>    |- ( ph -> ( x e. Y , y e. W |-> A ) e. ( ( K tX N ) Cn L ) )
Theorem	cnmptcom 14466*	The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
|- ( ph -> J e. (TopOn ` X ) )   &    |- ( ph -> K e. (TopOn ` Y ) )   &    |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )   =>    |- ( ph -> ( y e. Y , x e. X |-> A ) e. ( ( K tX J ) Cn L ) )
Theorem	imasnopn 14467	If a relation graph is open, then an image set of a singleton is also open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.)
|- X = U. J   =>    |- ( ( ( J e. Top /\ K e. Top ) /\ ( R e. ( J tX K ) /\ A e. X ) ) -> ( R " { A } ) e. K )
9.1.10  Homeomorphisms
Syntax	chmeo 14468	Extend class notation with the class of all homeomorphisms.
class Homeo
Definition	df-hmeo 14469*	Function returning all the homeomorphisms from topology j to topology k. (Contributed by FL, 14-Feb-2007.)
|- Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
Theorem	hmeofn 14470	The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- Homeo Fn ( Top X. Top )
Theorem	hmeofvalg 14471*	The set of all the homeomorphisms between two topologies. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ( J e. Top /\ K e. Top ) -> ( J Homeo K ) = { f e. ( J Cn K ) | `' f e. ( K Cn J ) } )
Theorem	ishmeo 14472	The predicate F is a homeomorphism between topology J and topology K. Proposition of [BourbakiTop1] p. I.2. (Contributed by FL, 14-Feb-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( F e. ( J Homeo K ) <-> ( F e. ( J Cn K ) /\ `' F e. ( K Cn J ) ) )
Theorem	hmeocn 14473	A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
Theorem	hmeocnvcn 14474	The converse of a homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( F e. ( J Homeo K ) -> `' F e. ( K Cn J ) )
Theorem	hmeocnv 14475	The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( F e. ( J Homeo K ) -> `' F e. ( K Homeo J ) )
Theorem	hmeof1o2 14476	A homeomorphism is a 1-1-onto mapping. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) /\ F e. ( J Homeo K ) ) -> F : X -1-1-onto-> Y )
Theorem	hmeof1o 14477	A homeomorphism is a 1-1-onto mapping. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 30-May-2014.)
|- X = U. J   &    |- Y = U. K   =>    |- ( F e. ( J Homeo K ) -> F : X -1-1-onto-> Y )
Theorem	hmeoima 14478	The image of an open set by a homeomorphism is an open set. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 22-Aug-2015.)
|- ( ( F e. ( J Homeo K ) /\ A e. J ) -> ( F " A ) e. K )
Theorem	hmeoopn 14479	Homeomorphisms preserve openness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. J <-> ( F " A ) e. K ) )
Theorem	hmeocld 14480	Homeomorphisms preserve closedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( A e. ( Clsd ` J ) <-> ( F " A ) e. ( Clsd ` K ) ) )
Theorem	hmeontr 14481	Homeomorphisms preserve interiors. (Contributed by Mario Carneiro, 25-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ A C_ X ) -> ( ( int ` K ) ` ( F " A ) ) = ( F " ( ( int ` J ) ` A ) ) )
Theorem	hmeoimaf1o 14482*	The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- G = ( x e. J |-> ( F " x ) )   =>    |- ( F e. ( J Homeo K ) -> G : J -1-1-onto-> K )
Theorem	hmeores 14483	The restriction of a homeomorphism is a homeomorphism. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
|- X = U. J   =>    |- ( ( F e. ( J Homeo K ) /\ Y C_ X ) -> ( F |` Y ) e. ( ( J ↾t Y ) Homeo ( K ↾t ( F " Y ) ) ) )
Theorem	hmeoco 14484	The composite of two homeomorphisms is a homeomorphism. (Contributed by FL, 9-Mar-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|- ( ( F e. ( J Homeo K ) /\ G e. ( K Homeo L ) ) -> ( G o. F ) e. ( J Homeo L ) )
Theorem	idhmeo 14485	The identity function is a homeomorphism. (Contributed by FL, 14-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
|- ( J e. (TopOn ` X ) -> ( _I |` X ) e. ( J Homeo J ) )
Theorem	hmeocnvb 14486	The converse of a homeomorphism is a homeomorphism. (Contributed by FL, 5-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.)
|- ( Rel F -> ( `' F e. ( J Homeo K ) <-> F e. ( K Homeo J ) ) )
Theorem	txhmeo 14487*	Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- X = U. J   &    |- Y = U. K   &    |- ( ph -> F e. ( J Homeo L ) )   &    |- ( ph -> G e. ( K Homeo M ) )   =>    |- ( ph -> ( x e. X , y e. Y |-> <. ( F ` x ) , ( G ` y ) >. ) e. ( ( J tX K ) Homeo ( L tX M ) ) )
Theorem	txswaphmeolem 14488*	Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( y e. Y , x e. X |-> <. x , y >. ) o. ( x e. X , y e. Y |-> <. y , x >. ) ) = ( _I |` ( X X. Y ) )
Theorem	txswaphmeo 14489*	There is a homeomorphism from X X. Y to Y X. X. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- ( ( J e. (TopOn ` X ) /\ K e. (TopOn ` Y ) ) -> ( x e. X , y e. Y |-> <. y , x >. ) e. ( ( J tX K ) Homeo ( K tX J ) ) )
9.2  Metric spaces
9.2.1  Pseudometric spaces
Theorem	psmetrel 14490	The class of pseudometrics is a relation. (Contributed by Jim Kingdon, 24-Apr-2023.)
|- Rel PsMet
Theorem	ispsmet 14491*	Express the predicate " D is a pseudometric". (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( X e. V -> ( D e. (PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
Theorem	psmetdmdm 14492	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> X = dom dom D )
Theorem	psmetf 14493	The distance function of a pseudometric as a function. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> RR* )
Theorem	psmetcl 14494	Closure of the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	psmet0 14495	The distance function of a pseudometric space is zero if its arguments are equal. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X ) -> ( A D A ) = 0 )
Theorem	psmettri2 14496	Triangle inequality for the distance function of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
Theorem	psmetsym 14497	The distance function of a pseudometric is symmetrical. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	psmettri 14498	Triangle inequality for the distance function of a pseudometric space. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
Theorem	psmetge0 14499	The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon, 19-Apr-2023.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	psmetxrge0 14500	The distance function of a pseudometric space is a function into the nonnegative extended real numbers. (Contributed by Thierry Arnoux, 24-Feb-2018.)
|- ( D e. (PsMet ` X ) -> D : ( X X. X ) --> ( 0 [,] +oo ) )