Theorem metxmet 23485

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

Syntax hints:   → wi 4   ∈ wcel 2110   × cxp 5588  ⟶wf 6428  ‘cfv 6432  ℝcr 10871  ∞Metcxmet 20580  Metcmet 20581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582  ax-cnex 10928  ax-resscn 10929  ax-1cn 10930  ax-icn 10931  ax-addcl 10932  ax-mulcl 10934  ax-i2m1 10940

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-er 8481  df-map 8600  df-en 8717  df-dom 8718  df-sdom 8719  df-pnf 11012  df-mnf 11013  df-xr 11014  df-xadd 12848  df-xmet 20588  df-met 20589

This theorem is referenced by:  metdmdm  23487  meteq0  23490  mettri2  23492  met0  23494  metge0  23496  metsym  23501  metrtri  23508  metgt0  23510  metres2  23514  prdsmet  23521  imasf1omet  23527  blpnf  23548  bl2in  23551  isms2  23601  setsms  23633  tmsms  23641  metss2lem  23665  metss2  23666  methaus  23674  dscopn  23727  ngpocelbl  23866  cnxmet  23934  rexmet  23952  metdcn2  24000  metdsre  24014  metdscn2  24018  lebnumlem1  24122  lebnumlem2  24123  lebnumlem3  24124  lebnum  24125  xlebnum  24126  cmetcaulem  24450  cmetcau  24451  iscmet3lem1  24453  iscmet3lem2  24454  iscmet3  24455  equivcfil  24461  equivcau  24462  metsscmetcld  24477  cmetss  24478  relcmpcmet  24480  cmpcmet  24481  cncmet  24484  bcthlem2  24487  bcthlem3  24488  bcthlem4  24489  bcthlem5  24490  bcth2  24492  bcth3  24493  cmetcusp1  24515  cmetcusp  24516  minveclem3  24591  imsxmet  29050  blocni  29163  ubthlem1  29228  ubthlem2  29229  minvecolem4a  29235  hhxmet  29533  hilxmet  29553  fmcncfil  31877  blssp  35910  lmclim2  35912  geomcau  35913  caures  35914  caushft  35915  sstotbnd2  35928  equivtotbnd  35932  isbndx  35936  isbnd3  35938  ssbnd  35942  totbndbnd  35943  prdstotbnd  35948  prdsbnd2  35949  heibor1lem  35963  heibor1  35964  heiborlem3  35967  heiborlem6  35970  heiborlem8  35972  heiborlem9  35973  heiborlem10  35974  heibor  35975  bfplem1  35976  bfplem2  35977  rrncmslem  35986  ismrer1  35992  reheibor  35993  metpsmet  42611  qndenserrnbllem  43806  qndenserrnbl  43807  qndenserrnopnlem  43809  rrndsxmet  43815  hoiqssbllem2  44132  hoiqssbl  44134  opnvonmbllem2  44142