Theorem metcl 24226

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 24224	. 2 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ)
2		fovcdm 7561	. 2 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)
3	1, 2	syl3an1 1163	1 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109   × cxp 5638  ⟶wf 6509  ‘cfv 6513  (class class class)co 7389  ℝcr 11073  Metcmet 21256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713  ax-cnex 11130  ax-resscn 11131

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3756  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-iota 6466  df-fun 6515  df-fn 6516  df-f 6517  df-fv 6521  df-ov 7392  df-oprab 7393  df-mpo 7394  df-map 8803  df-met 21264

This theorem is referenced by:  mettri2  24235  metrtri  24251  prdsmet  24264  imasf1omet  24270  blpnf  24291  bl2in  24294  mscl  24355  metss2lem  24405  methaus  24414  nmf2  24487  metdsre  24748  iscmet3lem1  25197  minveclem2  25332  minveclem3b  25334  minveclem3  25335  minveclem4  25338  minveclem7  25341  dvlog2lem  26567  vacn  30629  nmcvcn  30630  smcnlem  30632  blocni  30740  minvecolem2  30810  minvecolem3  30811  minvecolem4  30815  minvecolem7  30818  metf1o  37744  mettrifi  37746  lmclim2  37747  geomcau  37748  isbnd3  37773  isbnd3b  37774  ssbnd  37777  totbndbnd  37778  equivbnd  37779  prdsbnd  37782  heibor1lem  37798  heiborlem6  37805  bfplem1  37811  bfplem2  37812  bfp  37813  rrncmslem  37821  rrnequiv  37824  rrntotbnd  37825  ioorrnopnlem  46295