Theorem metxmet 22946

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

Syntax hints:   → wi 4   ∈ wcel 2114   × cxp 5555  ⟶wf 6353  ‘cfv 6357  ℝcr 10538  ∞Metcxmet 20532  Metcmet 20533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-mulcl 10601  ax-i2m1 10607

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-er 8291  df-map 8410  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-xadd 12511  df-xmet 20540  df-met 20541

This theorem is referenced by:  metdmdm  22948  meteq0  22951  mettri2  22953  met0  22955  metge0  22957  metsym  22962  metrtri  22969  metgt0  22971  metres2  22975  prdsmet  22982  imasf1omet  22988  blpnf  23009  bl2in  23012  isms2  23062  setsms  23092  tmsms  23099  metss2lem  23123  metss2  23124  methaus  23132  dscopn  23185  ngpocelbl  23315  cnxmet  23383  rexmet  23401  metdcn2  23449  metdsre  23463  metdscn2  23467  lebnumlem1  23567  lebnumlem2  23568  lebnumlem3  23569  lebnum  23570  xlebnum  23571  cmetcaulem  23893  cmetcau  23894  iscmet3lem1  23896  iscmet3lem2  23897  iscmet3  23898  equivcfil  23904  equivcau  23905  metsscmetcld  23920  cmetss  23921  relcmpcmet  23923  cmpcmet  23924  cncmet  23927  bcthlem2  23930  bcthlem3  23931  bcthlem4  23932  bcthlem5  23933  bcth2  23935  bcth3  23936  cmetcusp1  23958  cmetcusp  23959  minveclem3  24034  imsxmet  28471  blocni  28584  ubthlem1  28649  ubthlem2  28650  minvecolem4a  28656  hhxmet  28954  hilxmet  28974  fmcncfil  31176  blssp  35033  lmclim2  35035  geomcau  35036  caures  35037  caushft  35038  sstotbnd2  35054  equivtotbnd  35058  isbndx  35062  isbnd3  35064  ssbnd  35068  totbndbnd  35069  prdstotbnd  35074  prdsbnd2  35075  heibor1lem  35089  heibor1  35090  heiborlem3  35093  heiborlem6  35096  heiborlem8  35098  heiborlem9  35099  heiborlem10  35100  heibor  35101  bfplem1  35102  bfplem2  35103  rrncmslem  35112  ismrer1  35118  reheibor  35119  metpsmet  41364  qndenserrnbllem  42586  qndenserrnbl  42587  qndenserrnopnlem  42589  rrndsxmet  42595  hoiqssbllem2  42912  hoiqssbl  42914  opnvonmbllem2  42922