Theorem xmetcl 24273

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2113   × cxp 5620  ⟶wf 6486  ‘cfv 6490  (class class class)co 7356  ℝ^*cxr 11163  ∞Metcxmet 21292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-map 8763  df-xr 11168  df-xmet 21300

This theorem is referenced by:  xmetge0  24286  xmetlecl  24288  xmetsym  24289  xmetrtri  24297  xmetrtri2  24298  xmetgt0  24300  prdsdsf  24309  prdsxmetlem  24310  imasdsf1olem  24315  imasf1oxmet  24317  xpsdsval  24323  xblpnf  24338  bldisj  24340  blgt0  24341  xblss2  24344  blhalf  24347  xbln0  24356  blin  24363  blss  24367  xmscl  24404  prdsbl  24433  blsscls2  24446  blcld  24447  blcls  24448  comet  24455  stdbdxmet  24457  stdbdmet  24458  stdbdbl  24459  tmsxpsval2  24481  metcnpi3  24488  txmetcnp  24489  xrsmopn  24755  metdcnlem  24779  metdsf  24791  metdsge  24792  metdstri  24794  metdsle  24795  metdscnlem  24798  metnrmlem1  24802  metnrmlem3  24804  lmnn  25217  iscfil2  25220  iscau3  25232  dvlip2  25954  heicant  37795