Theorem metxmet 23395

Description: A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)

Assertion

Ref	Expression
metxmet	⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))

Proof of Theorem metxmet

Step	Hyp	Ref	Expression
1		ismet2 23394	. 2 ⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ))
2	1	simplbi 497	1 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))

Syntax hints:   → wi 4   ∈ wcel 2108   × cxp 5578  ⟶wf 6414  ‘cfv 6418  ℝcr 10801  ∞Metcxmet 20495  Metcmet 20496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-i2m1 10870

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-map 8575  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-xadd 12778  df-xmet 20503  df-met 20504

This theorem is referenced by:  metdmdm  23397  meteq0  23400  mettri2  23402  met0  23404  metge0  23406  metsym  23411  metrtri  23418  metgt0  23420  metres2  23424  prdsmet  23431  imasf1omet  23437  blpnf  23458  bl2in  23461  isms2  23511  setsms  23541  tmsms  23549  metss2lem  23573  metss2  23574  methaus  23582  dscopn  23635  ngpocelbl  23774  cnxmet  23842  rexmet  23860  metdcn2  23908  metdsre  23922  metdscn2  23926  lebnumlem1  24030  lebnumlem2  24031  lebnumlem3  24032  lebnum  24033  xlebnum  24034  cmetcaulem  24357  cmetcau  24358  iscmet3lem1  24360  iscmet3lem2  24361  iscmet3  24362  equivcfil  24368  equivcau  24369  metsscmetcld  24384  cmetss  24385  relcmpcmet  24387  cmpcmet  24388  cncmet  24391  bcthlem2  24394  bcthlem3  24395  bcthlem4  24396  bcthlem5  24397  bcth2  24399  bcth3  24400  cmetcusp1  24422  cmetcusp  24423  minveclem3  24498  imsxmet  28955  blocni  29068  ubthlem1  29133  ubthlem2  29134  minvecolem4a  29140  hhxmet  29438  hilxmet  29458  fmcncfil  31783  blssp  35841  lmclim2  35843  geomcau  35844  caures  35845  caushft  35846  sstotbnd2  35859  equivtotbnd  35863  isbndx  35867  isbnd3  35869  ssbnd  35873  totbndbnd  35874  prdstotbnd  35879  prdsbnd2  35880  heibor1lem  35894  heibor1  35895  heiborlem3  35898  heiborlem6  35901  heiborlem8  35903  heiborlem9  35904  heiborlem10  35905  heibor  35906  bfplem1  35907  bfplem2  35908  rrncmslem  35917  ismrer1  35923  reheibor  35924  metpsmet  42530  qndenserrnbllem  43725  qndenserrnbl  43726  qndenserrnopnlem  43728  rrndsxmet  43734  hoiqssbllem2  44051  hoiqssbl  44053  opnvonmbllem2  44061