Theorem metcl 23722

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	⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)

Proof of Theorem metcl

Step	Hyp	Ref	Expression
1		metf 23720	. 2 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ)
2		fovcdm 7529	. 2 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)
3	1, 2	syl3an1 1163	1 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2106   × cxp 5636  ⟶wf 6497  ‘cfv 6501  (class class class)co 7362  ℝcr 11059  Metcmet 20819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-cnex 11116  ax-resscn 11117

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-map 8774  df-met 20827

This theorem is referenced by:  mettri2  23731  metrtri  23747  prdsmet  23760  imasf1omet  23766  blpnf  23787  bl2in  23790  mscl  23851  metss2lem  23904  methaus  23913  nmf2  23986  metdsre  24253  iscmet3lem1  24692  minveclem2  24827  minveclem3b  24829  minveclem3  24830  minveclem4  24833  minveclem7  24836  dvlog2lem  26044  vacn  29699  nmcvcn  29700  smcnlem  29702  blocni  29810  minvecolem2  29880  minvecolem3  29881  minvecolem4  29885  minvecolem7  29888  metf1o  36287  mettrifi  36289  lmclim2  36290  geomcau  36291  isbnd3  36316  isbnd3b  36317  ssbnd  36320  totbndbnd  36321  equivbnd  36322  prdsbnd  36325  heibor1lem  36341  heiborlem6  36348  bfplem1  36354  bfplem2  36355  bfp  36356  rrncmslem  36364  rrnequiv  36367  rrntotbnd  36368  ioorrnopnlem  44665