Theorem metxmet 24359

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

Syntax hints:   → wi 4   ∈ wcel 2105   × cxp 5686  ⟶wf 6558  ‘cfv 6562  ℝcr 11151  ∞Metcxmet 21366  Metcmet 21367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-i2m1 11220

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-xadd 13152  df-xmet 21374  df-met 21375

This theorem is referenced by:  metdmdm  24361  meteq0  24364  mettri2  24366  met0  24368  metge0  24370  metsym  24375  metrtri  24382  metgt0  24384  metres2  24388  prdsmet  24395  imasf1omet  24401  blpnf  24422  bl2in  24425  isms2  24475  setsms  24507  tmsms  24515  metss2lem  24539  metss2  24540  methaus  24548  dscopn  24601  ngpocelbl  24740  cnxmet  24808  rexmet  24826  metdcn2  24874  metdsre  24888  metdscn2  24892  lebnumlem1  25006  lebnumlem2  25007  lebnumlem3  25008  lebnum  25009  xlebnum  25010  cmetcaulem  25335  cmetcau  25336  iscmet3lem1  25338  iscmet3lem2  25339  iscmet3  25340  equivcfil  25346  equivcau  25347  metsscmetcld  25362  cmetss  25363  relcmpcmet  25365  cmpcmet  25366  cncmet  25369  bcthlem2  25372  bcthlem3  25373  bcthlem4  25374  bcthlem5  25375  bcth2  25377  bcth3  25378  cmetcusp1  25400  cmetcusp  25401  minveclem3  25476  imsxmet  30720  blocni  30833  ubthlem1  30898  ubthlem2  30899  minvecolem4a  30905  hhxmet  31203  hilxmet  31223  fmcncfil  33891  blssp  37742  lmclim2  37744  geomcau  37745  caures  37746  caushft  37747  sstotbnd2  37760  equivtotbnd  37764  isbndx  37768  isbnd3  37770  ssbnd  37774  totbndbnd  37775  prdstotbnd  37780  prdsbnd2  37781  heibor1lem  37795  heibor1  37796  heiborlem3  37799  heiborlem6  37802  heiborlem8  37804  heiborlem9  37805  heiborlem10  37806  heibor  37807  bfplem1  37808  bfplem2  37809  rrncmslem  37818  ismrer1  37824  reheibor  37825  metpsmet  45030  qndenserrnbllem  46249  qndenserrnbl  46250  qndenserrnopnlem  46252  rrndsxmet  46258  hoiqssbllem2  46578  hoiqssbl  46580  opnvonmbllem2  46588