Theorem metxmet 24472

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

Syntax hints:   → wi 4   ∈ wcel 2143   × cxp 5661  ⟶wf 6534  ‘cfv 6538  ℝcr 11100  ∞Metcxmet 21488  Metcmet 21489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-i2m1 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8695  df-map 8827  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-xadd 13139  df-xmet 21496  df-met 21497

This theorem is referenced by:  metdmdm  24474  meteq0  24477  mettri2  24479  met0  24481  metge0  24483  metsym  24488  metrtri  24495  metgt0  24497  metres2  24501  prdsmet  24508  imasf1omet  24514  blpnf  24535  bl2in  24538  isms2  24588  setsms  24618  tmsms  24625  metss2lem  24649  metss2  24650  methaus  24658  dscopn  24711  ngpocelbl  24842  cnxmet  24910  rexmet  24929  metdcn2  24978  metdsre  24992  metdscn2  24996  lebnumlem1  25101  lebnumlem2  25102  lebnumlem3  25103  lebnum  25104  xlebnum  25105  cmetcaulem  25428  cmetcau  25429  iscmet3lem1  25431  iscmet3lem2  25432  iscmet3  25433  equivcfil  25439  equivcau  25440  metsscmetcld  25455  cmetss  25456  relcmpcmet  25458  cmpcmet  25459  cncmet  25462  bcthlem2  25465  bcthlem3  25466  bcthlem4  25467  bcthlem5  25468  bcth2  25470  bcth3  25471  cmetcusp1  25493  cmetcusp  25494  minveclem3  25569  imsxmet  31025  blocni  31138  ubthlem1  31203  ubthlem2  31204  minvecolem4a  31210  hhxmet  31508  hilxmet  31528  fmcncfil  34302  blssp  38388  lmclim2  38390  geomcau  38391  caures  38392  caushft  38393  sstotbnd2  38406  equivtotbnd  38410  isbndx  38414  isbnd3  38416  ssbnd  38420  totbndbnd  38421  prdstotbnd  38426  prdsbnd2  38427  heibor1lem  38441  heibor1  38442  heiborlem3  38445  heiborlem6  38448  heiborlem8  38450  heiborlem9  38451  heiborlem10  38452  heibor  38453  bfplem1  38454  bfplem2  38455  rrncmslem  38464  ismrer1  38470  reheibor  38471  metpsmet  45792  qndenserrnbllem  46991  qndenserrnbl  46992  qndenserrnopnlem  46994  rrndsxmet  47000  hoiqssbllem2  47320  hoiqssbl  47322  opnvonmbllem2  47330