Theorem metcl 24367

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2108   × cxp 5691  ⟶wf 6565  ‘cfv 6569  (class class class)co 7438  ℝcr 11161  Metcmet 21377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5305  ax-nul 5315  ax-pow 5374  ax-pr 5441  ax-un 7761  ax-cnex 11218  ax-resscn 11219

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3483  df-sbc 3795  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4916  df-br 5152  df-opab 5214  df-mpt 5235  df-id 5587  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-iota 6522  df-fun 6571  df-fn 6572  df-f 6573  df-fv 6577  df-ov 7441  df-oprab 7442  df-mpo 7443  df-map 8876  df-met 21385

This theorem is referenced by:  mettri2  24376  metrtri  24392  prdsmet  24405  imasf1omet  24411  blpnf  24432  bl2in  24435  mscl  24496  metss2lem  24549  methaus  24558  nmf2  24631  metdsre  24900  iscmet3lem1  25350  minveclem2  25485  minveclem3b  25487  minveclem3  25488  minveclem4  25491  minveclem7  25494  dvlog2lem  26720  vacn  30739  nmcvcn  30740  smcnlem  30742  blocni  30850  minvecolem2  30920  minvecolem3  30921  minvecolem4  30925  minvecolem7  30928  metf1o  37756  mettrifi  37758  lmclim2  37759  geomcau  37760  isbnd3  37785  isbnd3b  37786  ssbnd  37789  totbndbnd  37790  equivbnd  37791  prdsbnd  37794  heibor1lem  37810  heiborlem6  37817  bfplem1  37823  bfplem2  37824  bfp  37825  rrncmslem  37833  rrnequiv  37836  rrntotbnd  37837  ioorrnopnlem  46288