Theorem msxms 24579

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

Syntax hints:   → wi 4   ∈ wcel 2149   × cxp 5660   ↾ cres 5664  ‘cfv 6537  Basecbs 17268  distcds 17318  TopOpenctopn 17473  Metcmet 21476  ∞MetSpcxms 24442  MetSpcms 24443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-res 5674  df-iota 6493  df-fv 6545  df-ms 24446

This theorem is referenced by:  mstps  24580  imasf1oms  24615  ressms  24651  prdsms  24656  ngpxms  24726  ngptgp  24761  nlmvscnlem2  24810  nlmvscn  24812  nrginvrcn  24817  nghmcn  24870  cnfldxms  24901  nmhmcn  25247  ipcnlem2  25371  ipcn  25373  nglmle  25429  cmetcusp1  25480  dya2icoseg2  34612