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

Theorem xmetcl 17948
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 17946 . 2  |-  ( D  e.  ( * Met `  X )  ->  D : ( X  X.  X ) --> RR* )
2 fovrn 6032 . 2  |-  ( ( D : ( X  X.  X ) --> RR* 
/\  A  e.  X  /\  B  e.  X
)  ->  ( A D B )  e.  RR* )
31, 2syl3an1 1215 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 934    e. wcel 1701    X. cxp 4724   -->wf 5288   ` cfv 5292  (class class class)co 5900   RR*cxr 8911   * Metcxmt 16418
This theorem is referenced by:  xmetge0  17961  xmetlecl  17963  xmetsym  17964  xmetrtri  17971  xmetrtri2  17972  xmetgt0  17974  prdsdsf  17983  prdsxmetlem  17984  imasdsf1olem  17989  imasf1oxmet  17991  xpsdsval  17997  xblpnf  18005  bldisj  18007  blgt0  18008  xblss2  18010  blhalf  18012  xbln0  18017  blin  18022  blss  18024  xmscl  18060  prdsbl  18089  blsscls2  18102  blcld  18103  blcls  18104  comet  18111  stdbdxmet  18113  stdbdmet  18114  stdbdbl  18115  tmsxpsval2  18137  metcnpi3  18144  txmetcnp  18145  xrsmopn  18370  metdcnlem  18393  metdsf  18404  metdsge  18405  metdstri  18407  metdsle  18408  metdscnlem  18411  metnrmlem1  18415  metnrmlem3  18417  lmnn  18742  iscfil2  18745  iscau3  18757  dvlip2  19395  blval2  23506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-cnex 8838  ax-resscn 8839
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-map 6817  df-xr 8916  df-xmet 16425
  Copyright terms: Public domain W3C validator