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	txvalex 14801	Existence of the binary topological product. If R and S are known to be topologies, see txtop 14807. (Contributed by Jim Kingdon, 3-Aug-2023.)
|- ( ( R e. V /\ S e. W ) -> ( R tX S ) e. _V )
Theorem	txval 14802*	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 14803*	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 14804*	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 14805*	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 14806*	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 14807	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 14808	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 14809	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 14810	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 14811	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 14812	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 14813	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 14814	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 14815	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 14816	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 14817	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 14818*	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 14819*	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 14820*	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 14821*	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 14822	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 14823	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 14824	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 14825*	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 14826*	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 14827*	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 14828*	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 14829*	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 14830*	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 14831*	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 14832*	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 14833*	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 14834*	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 14835*	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 14836*	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 14837*	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 14838*	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 14839*	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 14840*	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 14841*	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 14842*	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 14843*	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 14844*	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 14845*	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 14846	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 14847	Extend class notation with the class of all homeomorphisms.
class Homeo
Definition	df-hmeo 14848*	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 14849	The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- Homeo Fn ( Top X. Top )
Theorem	hmeofvalg 14850*	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 14851	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 14852	A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
Theorem	hmeocnvcn 14853	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 14854	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 14855	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 14856	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 14857	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 14858	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 14859	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 14860	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 14861*	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 14862	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 14863	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 14864	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 14865	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 14866*	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 14867*	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 14868*	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 14869	The class of pseudometrics is a relation. (Contributed by Jim Kingdon, 24-Apr-2023.)
|- Rel PsMet
Theorem	ispsmet 14870*	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 14871	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> X = dom dom D )
Theorem	psmetf 14872	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 14873	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 14874	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 14875	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 14876	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 14877	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 14878	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 14879	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 ) )
Theorem	psmetres2 14880	Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)
|- ( ( D e. (PsMet ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. (PsMet ` R ) )
Theorem	psmetlecl 14881	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Thierry Arnoux, 11-Mar-2018.)
|- ( ( D e. (PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR )
Theorem	distspace 14882	A set X together with a (distance) function D which is a pseudometric is a distance space (according to E. Deza, M.M. Deza: "Dictionary of Distances", Elsevier, 2006), i.e. a (base) set X equipped with a distance D, which is a mapping of two elements of the base set to the (extended) reals and which is nonnegative, symmetric and equal to 0 if the two elements are equal. (Contributed by AV, 15-Oct-2021.) (Revised by AV, 5-Jul-2022.)
|- ( ( D e. (PsMet ` X ) /\ A e. X /\ B e. X ) -> ( ( D : ( X X. X ) --> RR* /\ ( A D A ) = 0 ) /\ ( 0 <_ ( A D B ) /\ ( A D B ) = ( B D A ) ) ) )
9.2.2  Basic metric space properties
Syntax	cxms 14883	Extend class notation with the class of extended metric spaces.
class *MetSp
Syntax	cms 14884	Extend class notation with the class of metric spaces.
class MetSp
Syntax	ctms 14885	Extend class notation with the function mapping a metric to the metric space it defines.
class toMetSp
Definition	df-xms 14886	Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
Definition	df-ms 14887	Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006.)
|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
Definition	df-tms 14888	Define the function mapping a metric to the metric space which it defines. (Contributed by Mario Carneiro, 2-Sep-2015.)
|- toMetSp = ( d e. U. ran *Met |-> ( { <. ( Base ` ndx ) , dom dom d >. , <. ( dist ` ndx ) , d >. } sSet <. (TopSet ` ndx ) , ( MetOpen ` d ) >. ) )
Theorem	metrel 14889	The class of metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.)
|- Rel Met
Theorem	xmetrel 14890	The class of extended metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.)
|- Rel *Met
Theorem	ismet 14891*	Express the predicate " D is a metric". (Contributed by NM, 25-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( X e. A -> ( D e. ( Met ` X ) <-> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) ) )
Theorem	isxmet 14892*	Express the predicate " D is an extended metric". (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( X e. A -> ( D e. ( *Met ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) )
Theorem	ismeti 14893*	Properties that determine a metric. (Contributed by NM, 17-Nov-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- X e. _V   &    |- D : ( X X. X ) --> RR   &    |- ( ( x e. X /\ y e. X ) -> ( ( x D y ) = 0 <-> x = y ) )   &    |- ( ( x e. X /\ y e. X /\ z e. X ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )   =>    |- D e. ( Met ` X )
Theorem	isxmetd 14894*	Properties that determine an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> X e. _V )   &    |- ( ph -> D : ( X X. X ) --> RR* )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) = 0 <-> x = y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) )   =>    |- ( ph -> D e. ( *Met ` X ) )
Theorem	isxmet2d 14895*	It is safe to only require the triangle inequality when the values are real (so that we can use the standard addition over the reals), but in this case the nonnegativity constraint cannot be deduced and must be provided separately. (Counterexample: D ( x , y ) = if ( x = y , 0 , -oo ) satisfies all hypotheses except nonnegativity.) (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ph -> X e. _V )   &    |- ( ph -> D : ( X X. X ) --> RR* )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> 0 <_ ( x D y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( x D y ) <_ 0 <-> x = y ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) /\ ( ( z D x ) e. RR /\ ( z D y ) e. RR ) ) -> ( x D y ) <_ ( ( z D x ) + ( z D y ) ) )   =>    |- ( ph -> D e. ( *Met ` X ) )
Theorem	metflem 14896*	Lemma for metf 14898 and others. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( D e. ( Met ` X ) -> ( D : ( X X. X ) --> RR /\ A. x e. X A. y e. X ( ( ( x D y ) = 0 <-> x = y ) /\ A. z e. X ( x D y ) <_ ( ( z D x ) + ( z D y ) ) ) ) )
Theorem	xmetf 14897	Mapping of the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( *Met ` X ) -> D : ( X X. X ) --> RR* )
Theorem	metf 14898	Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.)
|- ( D e. ( Met ` X ) -> D : ( X X. X ) --> RR )
Theorem	xmetcl 14899	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
Theorem	metcl 14900	Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR )