Theorem msxms 24514

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

Syntax hints:   → wi 4   ∈ wcel 2142   × cxp 5645   ↾ cres 5649  ‘cfv 6521  Basecbs 17245  distcds 17295  TopOpenctopn 17450  Metcmet 21410  ∞MetSpcxms 24377  MetSpcms 24378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-res 5659  df-iota 6477  df-fv 6529  df-ms 24381

This theorem is referenced by:  mstps  24515  imasf1oms  24550  ressms  24586  prdsms  24591  ngpxms  24661  ngptgp  24696  nlmvscnlem2  24745  nlmvscn  24747  nrginvrcn  24752  nghmcn  24805  cnfldxms  24836  nmhmcn  25182  ipcnlem2  25306  ipcn  25308  nglmle  25364  cmetcusp1  25415  dya2icoseg2  34575