Theorem metcl 23485

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 23483	. 2 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ)
2		fovrn 7442	. 2 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)
3	1, 2	syl3an1 1162	1 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ)

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2106   × cxp 5587  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275  ℝcr 10870  Metcmet 20583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-ov 7278  df-oprab 7279  df-mpo 7280  df-map 8617  df-met 20591

This theorem is referenced by:  mettri2  23494  metrtri  23510  prdsmet  23523  imasf1omet  23529  blpnf  23550  bl2in  23553  mscl  23614  metss2lem  23667  methaus  23676  nmf2  23749  metdsre  24016  iscmet3lem1  24455  minveclem2  24590  minveclem3b  24592  minveclem3  24593  minveclem4  24596  minveclem7  24599  dvlog2lem  25807  vacn  29056  nmcvcn  29057  smcnlem  29059  blocni  29167  minvecolem2  29237  minvecolem3  29238  minvecolem4  29242  minvecolem7  29245  metf1o  35913  mettrifi  35915  lmclim2  35916  geomcau  35917  isbnd3  35942  isbnd3b  35943  ssbnd  35946  totbndbnd  35947  equivbnd  35948  prdsbnd  35951  heibor1lem  35967  heiborlem6  35974  bfplem1  35980  bfplem2  35981  bfp  35982  rrncmslem  35990  rrnequiv  35993  rrntotbnd  35994  ioorrnopnlem  43845