Theorem msxms 24410

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 2737	. . 3 ⊢ (TopOpen‘𝑀) = (TopOpen‘𝑀)
2		eqid 2737	. . 3 ⊢ (Base‘𝑀) = (Base‘𝑀)
3		eqid 2737	. . 3 ⊢ ((dist‘𝑀) ↾ ((Base‘𝑀) × (Base‘𝑀))) = ((dist‘𝑀) ↾ ((Base‘𝑀) × (Base‘𝑀)))
4	1, 2, 3	isms 24405	. 2 ⊢ (𝑀 ∈ MetSp ↔ (𝑀 ∈ ∞MetSp ∧ ((dist‘𝑀) ↾ ((Base‘𝑀) × (Base‘𝑀))) ∈ (Met‘(Base‘𝑀))))
5	4	simplbi 496	1 ⊢ (𝑀 ∈ MetSp → 𝑀 ∈ ∞MetSp)

Syntax hints:   → wi 4   ∈ wcel 2114   × cxp 5630   ↾ cres 5634  ‘cfv 6500  Basecbs 17148  distcds 17198  TopOpenctopn 17353  Metcmet 21307  ∞MetSpcxms 24273  MetSpcms 24274

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-ext 2709

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-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-res 5644  df-iota 6456  df-fv 6508  df-ms 24277

This theorem is referenced by:  mstps  24411  imasf1oms  24446  ressms  24482  prdsms  24487  ngpxms  24557  ngptgp  24592  nlmvscnlem2  24641  nlmvscn  24643  nrginvrcn  24648  nghmcn  24701  cnfldxms  24732  nmhmcn  25088  ipcnlem2  25212  ipcn  25214  nglmle  25270  cmetcusp1  25321  dya2icoseg2  34456