Theorem msxms 24340

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

Syntax hints:   → wi 4   ∈ wcel 2109   × cxp 5617   ↾ cres 5621  ‘cfv 6482  Basecbs 17120  distcds 17170  TopOpenctopn 17325  Metcmet 21247  ∞MetSpcxms 24203  MetSpcms 24204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-res 5631  df-iota 6438  df-fv 6490  df-ms 24207

This theorem is referenced by:  mstps  24341  imasf1oms  24376  ressms  24412  prdsms  24417  ngpxms  24487  ngptgp  24522  nlmvscnlem2  24571  nlmvscn  24573  nrginvrcn  24578  nghmcn  24631  cnfldxms  24662  nmhmcn  25018  ipcnlem2  25142  ipcn  25144  nglmle  25200  cmetcusp1  25251  dya2icoseg2  34246