Theorem msxms 24318

Description: A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.)

Assertion

Ref	Expression
msxms	⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp)

Proof of Theorem msxms

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ (TopOpen‘𝑀) = (TopOpen‘𝑀)
2		eqid 2729	. . 3 ⊢ (Base‘𝑀) = (Base‘𝑀)
3		eqid 2729	. . 3 ⊢ ((dist‘𝑀) ↾ ((Base‘𝑀) × (Base‘𝑀))) = ((dist‘𝑀) ↾ ((Base‘𝑀) × (Base‘𝑀)))
4	1, 2, 3	isms 24313	. 2 ⊢ (𝑀 ∈ MetSp ↔ (𝑀 ∈ ∞MetSp ∧ ((dist‘𝑀) ↾ ((Base‘𝑀) × (Base‘𝑀))) ∈ (Met‘(Base‘𝑀))))
5	4	simplbi 497	1 ⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp)

Syntax hints:   → wi 4   ∈ wcel 2109   × cxp 5629   ↾ cres 5633  ‘cfv 6499  Basecbs 17155  distcds 17205  TopOpenctopn 17360  Metcmet 21226  ∞MetSpcxms 24181  MetSpcms 24182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-res 5643  df-iota 6452  df-fv 6507  df-ms 24185

This theorem is referenced by:  mstps  24319  imasf1oms  24354  ressms  24390  prdsms  24395  ngpxms  24465  ngptgp  24500  nlmvscnlem2  24549  nlmvscn  24551  nrginvrcn  24556  nghmcn  24609  cnfldxms  24640  nmhmcn  24996  ipcnlem2  25120  ipcn  25122  nglmle  25178  cmetcusp1  25229  dya2icoseg2  34242