Theorem msxms 22671

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

Syntax hints:   → wi 4   ∈ wcel 2107   × cxp 5355   ↾ cres 5359  ‘cfv 6137  Basecbs 16259  distcds 16351  TopOpenctopn 16472  Metcmet 20132  ∞MetSpcxms 22534  MetSpcms 22535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-xp 5363  df-res 5369  df-iota 6101  df-fv 6145  df-ms 22538

This theorem is referenced by:  mstps  22672  imasf1oms  22707  ressms  22743  prdsms  22748  ngpxms  22817  ngptgp  22852  nlmvscnlem2  22901  nlmvscn  22903  nrginvrcn  22908  nghmcn  22961  cnfldxms  22992  nmhmcn  23331  ipcnlem2  23454  ipcn  23456  nglmle  23512  cmetcusp1  23563  dya2icoseg2  30942