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

Theorem metcl 19910
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 19908 . 2  |-  ( D  e.  ( Met `  X
)  ->  D :
( X  X.  X
) --> RR )
2 fovrn 6236 . 2  |-  ( ( D : ( X  X.  X ) --> RR 
/\  A  e.  X  /\  B  e.  X
)  ->  ( A D B )  e.  RR )
31, 2syl3an1 1251 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 965    e. wcel 1756    X. cxp 4841   -->wf 5417   ` cfv 5421  (class class class)co 6094   RRcr 9284   Metcme 17805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-cnex 9341  ax-resscn 9342
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-mpt 4355  df-id 4639  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-ov 6097  df-oprab 6098  df-mpt2 6099  df-map 7219  df-met 17814
This theorem is referenced by:  mettri2  19919  metrtri  19935  prdsmet  19948  imasf1omet  19954  blpnf  19975  bl2in  19978  mscl  20039  metss2lem  20089  methaus  20098  nmf2  20188  metdsre  20432  iscmet3lem1  20805  minveclem2  20916  minveclem3b  20918  minveclem3  20919  minveclem4  20922  minveclem7  20925  dvlog2lem  22100  vacn  24092  nmcvcn  24093  smcnlem  24095  blocni  24208  minvecolem2  24279  minvecolem3  24280  minvecolem4  24284  minvecolem7  24287  metf1o  28654  mettrifi  28656  lmclim2  28657  geomcau  28658  isbnd3  28686  isbnd3b  28687  ssbnd  28690  totbndbnd  28691  equivbnd  28692  prdsbnd  28695  heibor1lem  28711  heiborlem6  28718  bfplem1  28724  bfplem2  28725  bfp  28726  rrncmslem  28734  rrnequiv  28737  rrntotbnd  28738
  Copyright terms: Public domain W3C validator