Theorem metcl 24307

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114   × cxp 5622  ⟶wf 6488  ‘cfv 6492  (class class class)co 7360  ℝcr 11028  Metcmet 21330

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-map 8768  df-met 21338

This theorem is referenced by:  mettri2  24316  metrtri  24332  prdsmet  24345  imasf1omet  24351  blpnf  24372  bl2in  24375  mscl  24436  metss2lem  24486  methaus  24495  nmf2  24568  metdsre  24829  iscmet3lem1  25268  minveclem2  25403  minveclem3b  25405  minveclem3  25406  minveclem4  25409  minveclem7  25412  dvlog2lem  26629  vacn  30780  nmcvcn  30781  smcnlem  30783  blocni  30891  minvecolem2  30961  minvecolem3  30962  minvecolem4  30966  minvecolem7  30969  metf1o  38090  mettrifi  38092  lmclim2  38093  geomcau  38094  isbnd3  38119  isbnd3b  38120  ssbnd  38123  totbndbnd  38124  equivbnd  38125  prdsbnd  38128  heibor1lem  38144  heiborlem6  38151  bfplem1  38157  bfplem2  38158  bfp  38159  rrncmslem  38167  rrnequiv  38170  rrntotbnd  38171  ioorrnopnlem  46750