P. 151 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15001-15100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnmpt12 15001*	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 15002*	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 15003*	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 15004*	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 15005*	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 15006*	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 15007*	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 15008*	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 15009*	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 15010*	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 15011*	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 15012*	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 15013	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 15014	Extend class notation with the class of all homeomorphisms.
class Homeo
Definition	df-hmeo 15015*	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 15016	The set of homeomorphisms is a function on topologies. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- Homeo Fn ( Top X. Top )
Theorem	hmeofvalg 15017*	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 15018	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 15019	A homeomorphism is continuous. (Contributed by Mario Carneiro, 22-Aug-2015.)
|- ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
Theorem	hmeocnvcn 15020	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 15021	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 15022	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 15023	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 15024	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 15025	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 15026	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 15027	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 15028*	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 15029	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 15030	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 15031	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 15032	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 15033*	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 15034*	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 15035*	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 15036	The class of pseudometrics is a relation. (Contributed by Jim Kingdon, 24-Apr-2023.)
|- Rel PsMet
Theorem	ispsmet 15037*	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 15038	Recover the base set from a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. (PsMet ` X ) -> X = dom dom D )
Theorem	psmetf 15039	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 15040	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 15041	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 15042	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 15043	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 15044	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 15045	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 15046	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 15047	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 15048	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 15049	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 15050	Extend class notation with the class of extended metric spaces.
class *MetSp
Syntax	cms 15051	Extend class notation with the class of metric spaces.
class MetSp
Syntax	ctms 15052	Extend class notation with the function mapping a metric to the metric space it defines.
class toMetSp
Definition	df-xms 15053	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 15054	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 15055	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 15056	The class of metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.)
|- Rel Met
Theorem	xmetrel 15057	The class of extended metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.)
|- Rel *Met
Theorem	ismet 15058*	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 15059*	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 15060*	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 15061*	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 15062*	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 15063*	Lemma for metf 15065 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 15064	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 15065	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 15066	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 15067	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	ismet2 15068	An extended metric is a metric exactly when it takes real values for all values of the arguments. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( Met ` X ) <-> ( D e. ( *Met ` X ) /\ D : ( X X. X ) --> RR ) )
Theorem	metxmet 15069	A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
Theorem	xmetdmdm 15070	Recover the base set from an extended metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( D e. ( *Met ` X ) -> X = dom dom D )
Theorem	metdmdm 15071	Recover the base set from a metric. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( D e. ( Met ` X ) -> X = dom dom D )
Theorem	xmetunirn 15072	Two ways to express an extended metric on an unspecified base. (Contributed by Mario Carneiro, 13-Oct-2015.)
|- ( D e. U. ran *Met <-> D e. ( *Met ` dom dom D ) )
Theorem	xmeteq0 15073	The value of an extended metric is zero iff its arguments are equal. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )
Theorem	meteq0 15074	The value of a metric is zero iff its arguments are equal. Property M2 of [Kreyszig] p. 4. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( ( A D B ) = 0 <-> A = B ) )
Theorem	xmettri2 15075	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) +e ( C D B ) ) )
Theorem	mettri2 15076	Triangle inequality for the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ ( C e. X /\ A e. X /\ B e. X ) ) -> ( A D B ) <_ ( ( C D A ) + ( C D B ) ) )
Theorem	xmet0 15077	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )
Theorem	met0 15078	The distance function of a metric space is zero if its arguments are equal. Definition 14-1.1(a) of [Gleason] p. 223. (Contributed by NM, 30-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ A e. X ) -> ( A D A ) = 0 )
Theorem	xmetge0 15079	The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	metge0 15080	The distance function of a metric space is nonnegative. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
Theorem	xmetlecl 15081	Real closure of an extended metric value that is upper bounded by a real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR )
Theorem	xmetsym 15082	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	xmetpsmet 15083	An extended metric is a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- ( D e. ( *Met ` X ) -> D e. (PsMet ` X ) )
Theorem	xmettpos 15084	The distance function of an extended metric space is symmetric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( D e. ( *Met ` X ) -> tpos D = D )
Theorem	metsym 15085	The distance function of a metric space is symmetric. Definition 14-1.1(c) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) = ( B D A ) )
Theorem	xmettri 15086	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( C D B ) ) )
Theorem	mettri 15087	Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by NM, 27-Aug-2006.)
|- ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( C D B ) ) )
Theorem	xmettri3 15088	Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) +e ( B D C ) ) )
Theorem	mettri3 15089	Triangle inequality for the distance function of a metric space. (Contributed by NM, 13-Mar-2007.)
|- ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A D B ) <_ ( ( A D C ) + ( B D C ) ) )
Theorem	xmetrtri 15090	One half of the reverse triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A D C ) +e -e ( B D C ) ) <_ ( A D B ) )
Theorem	metrtri 15091	Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 21-Apr-2023.)
|- ( ( D e. ( Met ` X ) /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( abs ` ( ( A D C ) - ( B D C ) ) ) <_ ( A D B ) )
Theorem	metn0 15092	A metric space is nonempty iff its base set is nonempty. (Contributed by NM, 4-Oct-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( D e. ( Met ` X ) -> ( D =/= (/) <-> X =/= (/) ) )
Theorem	xmetres2 15093	Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( D e. ( *Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( *Met ` R ) )
Theorem	metreslem 15094	Lemma for metres 15097. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( dom D = ( X X. X ) -> ( D |` ( R X. R ) ) = ( D |` ( ( X i^i R ) X. ( X i^i R ) ) ) )
Theorem	metres2 15095	Lemma for metres 15097. (Contributed by FL, 12-Oct-2006.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
|- ( ( D e. ( Met ` X ) /\ R C_ X ) -> ( D |` ( R X. R ) ) e. ( Met ` R ) )
Theorem	xmetres 15096	A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( D e. ( *Met ` X ) -> ( D |` ( R X. R ) ) e. ( *Met ` ( X i^i R ) ) )
Theorem	metres 15097	A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- ( D e. ( Met ` X ) -> ( D |` ( R X. R ) ) e. ( Met ` ( X i^i R ) ) )
Theorem	0met 15098	The empty metric. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 14-Aug-2015.)
|- (/) e. ( Met ` (/) )
9.2.3  Metric space balls
Theorem	blfvalps 15099*	The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ( D e. (PsMet ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )
Theorem	blfval 15100*	The value of the ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) (Proof shortened by Thierry Arnoux, 11-Feb-2018.)
|- ( D e. ( *Met ` X ) -> ( ball ` D ) = ( x e. X , r e. RR* |-> { y e. X | ( x D y ) < r } ) )