Theorem msxms 24419

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

Syntax hints:   → wi 4   ∈ wcel 2114   × cxp 5629   ↾ cres 5633  ‘cfv 6498  Basecbs 17179  distcds 17229  TopOpenctopn 17384  Metcmet 21338  ∞MetSpcxms 24282  MetSpcms 24283

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-res 5643  df-iota 6454  df-fv 6506  df-ms 24286

This theorem is referenced by:  mstps  24420  imasf1oms  24455  ressms  24491  prdsms  24496  ngpxms  24566  ngptgp  24601  nlmvscnlem2  24650  nlmvscn  24652  nrginvrcn  24657  nghmcn  24710  cnfldxms  24741  nmhmcn  25087  ipcnlem2  25211  ipcn  25213  nglmle  25269  cmetcusp1  25320  dya2icoseg2  34422