Theorem msxms 24611

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

Syntax hints:   → wi 4   ∈ wcel 2143   × cxp 5659   ↾ cres 5663  ‘cfv 6536  Basecbs 17264  distcds 17314  TopOpenctopn 17469  Metcmet 21508  ∞MetSpcxms 24474  MetSpcms 24475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-res 5673  df-iota 6492  df-fv 6544  df-ms 24478

This theorem is referenced by:  mstps  24612  imasf1oms  24647  ressms  24683  prdsms  24688  ngpxms  24758  ngptgp  24793  nlmvscnlem2  24842  nlmvscn  24844  nrginvrcn  24849  nghmcn  24902  cnfldxms  24933  nmhmcn  25279  ipcnlem2  25403  ipcn  25405  nglmle  25461  cmetcusp1  25512  dya2icoseg2  34668