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

Theorem xmetcl 17823
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 17821 . 2  |-  ( D  e.  ( * Met `  X )  ->  D : ( X  X.  X ) --> RR* )
2 fovrn 5889 . 2  |-  ( ( D : ( X  X.  X ) --> RR* 
/\  A  e.  X  /\  B  e.  X
)  ->  ( A D B )  e.  RR* )
31, 2syl3an1 1220 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 6    /\ w3a 939    e. wcel 1621    X. cxp 4624   -->wf 4634   ` cfv 4638  (class class class)co 5757   RR*cxr 8799   * Metcxmt 16296
This theorem is referenced by:  xmetge0  17836  xmetlecl  17838  xmetsym  17839  xmetrtri  17846  xmetrtri2  17847  xmetgt0  17849  prdsdsf  17858  prdsxmetlem  17859  imasdsf1olem  17864  imasf1oxmet  17866  xpsdsval  17872  xblpnf  17880  bldisj  17882  blgt0  17883  xblss2  17885  blhalf  17887  xbln0  17892  blin  17897  blss  17899  xmscl  17935  prdsbl  17964  blsscls2  17977  blcld  17978  blcls  17979  comet  17986  stdbdxmet  17988  stdbdmet  17989  stdbdbl  17990  tmsxpsval2  18012  metcnpi3  18019  txmetcnp  18020  xrsmopn  18245  metdcnlem  18268  metdsf  18279  metdsge  18280  metdstri  18282  metdsle  18283  metdscnlem  18286  metnrmlem1  18290  metnrmlem3  18292  lmnn  18616  iscfil2  18619  iscau3  18631  dvlip2  19269
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pow 4126  ax-pr 4152  ax-un 4449  ax-cnex 8726  ax-resscn 8727
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-sbc 2936  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-mpt 4019  df-id 4246  df-xp 4640  df-rel 4641  df-cnv 4642  df-co 4643  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fun 4648  df-fn 4649  df-f 4650  df-fv 4654  df-ov 5760  df-oprab 5761  df-mpt2 5762  df-map 6707  df-xr 8804  df-xmet 16300
  Copyright terms: Public domain W3C validator