Theorem metxmet 22941

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

Syntax hints:   → wi 4   ∈ wcel 2111   × cxp 5517  ⟶wf 6320  ‘cfv 6324  ℝcr 10525  ∞Metcxmet 20076  Metcmet 20077

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-i2m1 10594

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-xadd 12496  df-xmet 20084  df-met 20085

This theorem is referenced by:  metdmdm  22943  meteq0  22946  mettri2  22948  met0  22950  metge0  22952  metsym  22957  metrtri  22964  metgt0  22966  metres2  22970  prdsmet  22977  imasf1omet  22983  blpnf  23004  bl2in  23007  isms2  23057  setsms  23087  tmsms  23094  metss2lem  23118  metss2  23119  methaus  23127  dscopn  23180  ngpocelbl  23310  cnxmet  23378  rexmet  23396  metdcn2  23444  metdsre  23458  metdscn2  23462  lebnumlem1  23566  lebnumlem2  23567  lebnumlem3  23568  lebnum  23569  xlebnum  23570  cmetcaulem  23892  cmetcau  23893  iscmet3lem1  23895  iscmet3lem2  23896  iscmet3  23897  equivcfil  23903  equivcau  23904  metsscmetcld  23919  cmetss  23920  relcmpcmet  23922  cmpcmet  23923  cncmet  23926  bcthlem2  23929  bcthlem3  23930  bcthlem4  23931  bcthlem5  23932  bcth2  23934  bcth3  23935  cmetcusp1  23957  cmetcusp  23958  minveclem3  24033  imsxmet  28475  blocni  28588  ubthlem1  28653  ubthlem2  28654  minvecolem4a  28660  hhxmet  28958  hilxmet  28978  fmcncfil  31284  blssp  35194  lmclim2  35196  geomcau  35197  caures  35198  caushft  35199  sstotbnd2  35212  equivtotbnd  35216  isbndx  35220  isbnd3  35222  ssbnd  35226  totbndbnd  35227  prdstotbnd  35232  prdsbnd2  35233  heibor1lem  35247  heibor1  35248  heiborlem3  35251  heiborlem6  35254  heiborlem8  35256  heiborlem9  35257  heiborlem10  35258  heibor  35259  bfplem1  35260  bfplem2  35261  rrncmslem  35270  ismrer1  35276  reheibor  35277  metpsmet  41727  qndenserrnbllem  42936  qndenserrnbl  42937  qndenserrnopnlem  42939  rrndsxmet  42945  hoiqssbllem2  43262  hoiqssbl  43264  opnvonmbllem2  43272