Theorem xmetcl 22938

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

Proof of Theorem xmetcl

Step	Hyp	Ref	Expression
1		xmetf 22936	. 2 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
2		fovrn 7298	. 2 ⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
3	1, 2	syl3an1 1160	1 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)

Syntax hints:   → wi 4   ∧ w3a 1084   ∈ wcel 2111   × cxp 5517  ⟶wf 6320  ‘cfv 6324  (class class class)co 7135  ℝ^*cxr 10663  ∞Metcxmet 20076

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-map 8391  df-xr 10668  df-xmet 20084

This theorem is referenced by:  xmetge0  22951  xmetlecl  22953  xmetsym  22954  xmetrtri  22962  xmetrtri2  22963  xmetgt0  22965  prdsdsf  22974  prdsxmetlem  22975  imasdsf1olem  22980  imasf1oxmet  22982  xpsdsval  22988  xblpnf  23003  bldisj  23005  blgt0  23006  xblss2  23009  blhalf  23012  xbln0  23021  blin  23028  blss  23032  xmscl  23069  prdsbl  23098  blsscls2  23111  blcld  23112  blcls  23113  comet  23120  stdbdxmet  23122  stdbdmet  23123  stdbdbl  23124  tmsxpsval2  23146  metcnpi3  23153  txmetcnp  23154  xrsmopn  23417  metdcnlem  23441  metdsf  23453  metdsge  23454  metdstri  23456  metdsle  23457  metdscnlem  23460  metnrmlem1  23464  metnrmlem3  23466  lmnn  23867  iscfil2  23870  iscau3  23882  dvlip2  24598  heicant  35092