Theorem xmetcl 24659

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

Step	Hyp	Ref	Expression
1		xmetf 24657	. 2 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
2		fovcdm 7595	. 2 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
3	1, 2	syl3an1 1181	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2144   × cxp 5649  ⟶wf 6539  ‘cfv 6543  (class class class)co 7424  ℝ^*cxr 11349  ∞Metcxmet 21672

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7427  df-oprab 7428  df-mpo 7429  df-map 8857  df-xr 11354  df-xmet 21680

This theorem is used by:  xmetge0  24672  xmetlecl  24674  xmetsym  24675  xmetrtri  24683  xmetrtri2  24684  xmetgt0  24686  prdsdsf  24695  prdsxmetlem  24696  imasdsf1olem  24701  imasf1oxmet  24703  xpsdsval  24709  xblpnf  24724  bldisj  24726  blgt0  24727  xblss2  24730  blhalf  24733  xbln0  24742  blin  24749  blss  24753  xmscl  24790  prdsbl  24819  blsscls2  24832  blcld  24833  blcls  24834  comet  24841  stdbdxmet  24843  stdbdmet  24844  stdbdbl  24845  tmsxpsval2  24867  metcnpi3  24874  txmetcnp  24875  xrsmopn  25141  metdcnlem  25165  metdsf  25177  metdsge  25178  metdstri  25180  metdsle  25181  metdscnlem  25184  metnrmlem1  25188  metnrmlem3  25190  lmnn  25593  iscfil2  25596  iscau3  25608  dvlip2  26324  heicant  38710