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

Theorem xmetcl 22414
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 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)

Proof of Theorem xmetcl
StepHypRef Expression
1 xmetf 22412 . 2 (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
2 fovrn 7001 . 2 ((𝐷:(𝑋 × 𝑋)⟶ℝ*𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
31, 2syl3an1 1202 1 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107  wcel 2155   × cxp 5274  wf 6063  cfv 6067  (class class class)co 6841  *cxr 10326  ∞Metcxmet 20003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-fv 6075  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-map 8061  df-xr 10331  df-xmet 20011
This theorem is referenced by:  xmetge0  22427  xmetlecl  22429  xmetsym  22430  xmetrtri  22438  xmetrtri2  22439  xmetgt0  22441  prdsdsf  22450  prdsxmetlem  22451  imasdsf1olem  22456  imasf1oxmet  22458  xpsdsval  22464  xblpnf  22479  bldisj  22481  blgt0  22482  xblss2  22485  blhalf  22488  xbln0  22497  blin  22504  blss  22508  xmscl  22545  prdsbl  22574  blsscls2  22587  blcld  22588  blcls  22589  comet  22596  stdbdxmet  22598  stdbdmet  22599  stdbdbl  22600  tmsxpsval2  22622  metcnpi3  22629  txmetcnp  22630  xrsmopn  22893  metdcnlem  22917  metdsf  22929  metdsge  22930  metdstri  22932  metdsle  22933  metdscnlem  22936  metnrmlem1  22940  metnrmlem3  22942  lmnn  23339  iscfil2  23342  iscau3  23354  dvlip2  24048  heicant  33800
  Copyright terms: Public domain W3C validator