Theorem metxmet 24344

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

Syntax hints:   → wi 4   ∈ wcel 2108   × cxp 5683  ⟶wf 6557  ‘cfv 6561  ℝcr 11154  ∞Metcxmet 21349  Metcmet 21350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-i2m1 11223

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-xadd 13155  df-xmet 21357  df-met 21358

This theorem is referenced by:  metdmdm  24346  meteq0  24349  mettri2  24351  met0  24353  metge0  24355  metsym  24360  metrtri  24367  metgt0  24369  metres2  24373  prdsmet  24380  imasf1omet  24386  blpnf  24407  bl2in  24410  isms2  24460  setsms  24492  tmsms  24500  metss2lem  24524  metss2  24525  methaus  24533  dscopn  24586  ngpocelbl  24725  cnxmet  24793  rexmet  24812  metdcn2  24861  metdsre  24875  metdscn2  24879  lebnumlem1  24993  lebnumlem2  24994  lebnumlem3  24995  lebnum  24996  xlebnum  24997  cmetcaulem  25322  cmetcau  25323  iscmet3lem1  25325  iscmet3lem2  25326  iscmet3  25327  equivcfil  25333  equivcau  25334  metsscmetcld  25349  cmetss  25350  relcmpcmet  25352  cmpcmet  25353  cncmet  25356  bcthlem2  25359  bcthlem3  25360  bcthlem4  25361  bcthlem5  25362  bcth2  25364  bcth3  25365  cmetcusp1  25387  cmetcusp  25388  minveclem3  25463  imsxmet  30711  blocni  30824  ubthlem1  30889  ubthlem2  30890  minvecolem4a  30896  hhxmet  31194  hilxmet  31214  fmcncfil  33930  blssp  37763  lmclim2  37765  geomcau  37766  caures  37767  caushft  37768  sstotbnd2  37781  equivtotbnd  37785  isbndx  37789  isbnd3  37791  ssbnd  37795  totbndbnd  37796  prdstotbnd  37801  prdsbnd2  37802  heibor1lem  37816  heibor1  37817  heiborlem3  37820  heiborlem6  37823  heiborlem8  37825  heiborlem9  37826  heiborlem10  37827  heibor  37828  bfplem1  37829  bfplem2  37830  rrncmslem  37839  ismrer1  37845  reheibor  37846  metpsmet  45096  qndenserrnbllem  46309  qndenserrnbl  46310  qndenserrnopnlem  46312  rrndsxmet  46318  hoiqssbllem2  46638  hoiqssbl  46640  opnvonmbllem2  46648