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

Theorem metcl 21129
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
metcl  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( A D B )  e.  RR )

Proof of Theorem metcl
StepHypRef Expression
1 metf 21127 . 2  |-  ( D  e.  ( Met `  X
)  ->  D :
( X  X.  X
) --> RR )
2 fovrn 6428 . 2  |-  ( ( D : ( X  X.  X ) --> RR 
/\  A  e.  X  /\  B  e.  X
)  ->  ( A D B )  e.  RR )
31, 2syl3an1 1265 1  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  B  e.  X )  ->  ( A D B )  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 976    e. wcel 1844    X. cxp 4823   -->wf 5567   ` cfv 5571  (class class class)co 6280   RRcr 9523   Metcme 18726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-cnex 9580  ax-resscn 9581
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-opab 4456  df-mpt 4457  df-id 4740  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-fv 5579  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-map 7461  df-met 18735
This theorem is referenced by:  mettri2  21138  metrtri  21154  prdsmet  21167  imasf1omet  21173  blpnf  21194  bl2in  21197  mscl  21258  metss2lem  21308  methaus  21317  nmf2  21407  metdsre  21651  iscmet3lem1  22024  minveclem2  22135  minveclem3b  22137  minveclem3  22138  minveclem4  22141  minveclem7  22144  dvlog2lem  23329  vacn  26031  nmcvcn  26032  smcnlem  26034  blocni  26147  minvecolem2  26218  minvecolem3  26219  minvecolem4  26223  minvecolem7  26226  metf1o  31543  mettrifi  31545  lmclim2  31546  geomcau  31547  isbnd3  31575  isbnd3b  31576  ssbnd  31579  totbndbnd  31580  equivbnd  31581  prdsbnd  31584  heibor1lem  31600  heiborlem6  31607  bfplem1  31613  bfplem2  31614  bfp  31615  rrncmslem  31623  rrnequiv  31626  rrntotbnd  31627
  Copyright terms: Public domain W3C validator