MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xmetcl Unicode version

Theorem xmetcl 18344
Description: Closure of the distance function of a metric space. Part of Property M1 of [Kreyszig] p. 3. (Contributed by NM, 30-Aug-2006.)
Assertion
Ref Expression
xmetcl  |-  ( ( D  e.  ( * Met `  X )  /\  A  e.  X  /\  B  e.  X
)  ->  ( A D B )  e.  RR* )

Proof of Theorem xmetcl
StepHypRef Expression
1 xmetf 18342 . 2  |-  ( D  e.  ( * Met `  X )  ->  D : ( X  X.  X ) --> RR* )
2 fovrn 6202 . 2  |-  ( ( D : ( X  X.  X ) --> RR* 
/\  A  e.  X  /\  B  e.  X
)  ->  ( A D B )  e.  RR* )
31, 2syl3an1 1217 1  |-  ( ( D  e.  ( * Met `  X )  /\  A  e.  X  /\  B  e.  X
)  ->  ( A D B )  e.  RR* )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    e. wcel 1725    X. cxp 4862   -->wf 5436   ` cfv 5440  (class class class)co 6067   RR*cxr 9103   * Metcxmt 16669
This theorem is referenced by:  xmetge0  18357  xmetlecl  18359  xmetsym  18360  xmetrtri  18368  xmetrtri2  18369  xmetgt0  18371  prdsdsf  18380  prdsxmetlem  18381  imasdsf1olem  18386  imasf1oxmet  18388  xpsdsval  18394  xblpnf  18409  bldisj  18411  blgt0  18412  xblss2  18415  blhalf  18418  xbln0  18427  blin  18434  blss  18438  xmscl  18475  prdsbl  18504  blsscls2  18517  blcld  18518  blcls  18519  comet  18526  stdbdxmet  18528  stdbdmet  18529  stdbdbl  18530  tmsxpsval2  18552  metcnpi3  18559  txmetcnp  18560  xrsmopn  18826  metdcnlem  18850  metdsf  18861  metdsge  18862  metdstri  18864  metdsle  18865  metdscnlem  18868  metnrmlem1  18872  metnrmlem3  18874  lmnn  19199  iscfil2  19202  iscau3  19214  dvlip2  19862
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pow 4364  ax-pr 4390  ax-un 4687  ax-cnex 9030  ax-resscn 9031
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-sbc 3149  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-mpt 4255  df-id 4485  df-xp 4870  df-rel 4871  df-cnv 4872  df-co 4873  df-dm 4874  df-rn 4875  df-iota 5404  df-fun 5442  df-fn 5443  df-f 5444  df-fv 5448  df-ov 6070  df-oprab 6071  df-mpt2 6072  df-map 7006  df-xr 9108  df-xmet 16678
  Copyright terms: Public domain W3C validator