Theorem metxmet 21949

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 21948	. 2 ⊢ (𝐷 ∈ (Met‘𝑋) ↔ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝐷:(𝑋 × 𝑋)⟶ℝ))
2	1	simplbi 475	1 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))

Syntax hints:   → wi 4   ∈ wcel 1977   × cxp 5036  ⟶wf 5800  ‘cfv 5804  ℝcr 9814  ∞Metcxmt 19552  Metcme 19553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-i2m1 9883

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-xadd 11823  df-xmet 19560  df-met 19561

This theorem is referenced by:  metdmdm  21951  meteq0  21954  mettri2  21956  met0  21958  metge0  21960  metsym  21965  metrtri  21972  metgt0  21974  metres2  21978  prdsmet  21985  imasf1omet  21991  blpnf  22012  bl2in  22015  isms2  22065  setsms  22095  tmsms  22102  metss2lem  22126  metss2  22127  methaus  22135  dscopn  22188  ngpocelbl  22318  cnxmet  22386  rexmet  22402  metdcn2  22450  metdsre  22464  metdscn2  22468  lebnumlem1  22568  lebnumlem2  22569  lebnumlem3  22570  lebnum  22571  xlebnum  22572  cmetcaulem  22894  cmetcau  22895  iscmet3lem1  22897  iscmet3lem2  22898  iscmet3  22899  equivcfil  22905  equivcau  22906  cmetss  22921  relcmpcmet  22923  cmpcmet  22924  cncmet  22927  bcthlem2  22930  bcthlem3  22931  bcthlem4  22932  bcthlem5  22933  bcth2  22935  bcth3  22936  cmetcusp1  22957  cmetcusp  22958  minveclem3  23008  imsxmet  26931  blocni  27044  ubthlem1  27110  ubthlem2  27111  minvecolem4a  27117  hhxmet  27416  hilxmet  27436  fmcncfil  29305  blssp  32722  lmclim2  32724  geomcau  32725  caures  32726  caushft  32727  sstotbnd2  32743  equivtotbnd  32747  isbndx  32751  isbnd3  32753  ssbnd  32757  totbndbnd  32758  prdstotbnd  32763  prdsbnd2  32764  heibor1lem  32778  heibor1  32779  heiborlem3  32782  heiborlem6  32785  heiborlem8  32787  heiborlem9  32788  heiborlem10  32789  heibor  32790  bfplem1  32791  bfplem2  32792  rrncmslem  32801  ismrer1  32807  reheibor  32808  metpsmet  38296  qndenserrnbllem  39190  qndenserrnbl  39191  qndenserrnopnlem  39193  rrndsxmet  39199  hoiqssbllem2  39513  hoiqssbl  39515  opnvonmbllem2  39523