Theorem metxmet 24250

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

Syntax hints:   → wi 4   ∈ wcel 2111   × cxp 5614  ⟶wf 6477  ‘cfv 6481  ℝcr 11005  ∞Metcxmet 21277  Metcmet 21278

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-i2m1 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-map 8752  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-xadd 13012  df-xmet 21285  df-met 21286

This theorem is referenced by:  metdmdm  24252  meteq0  24255  mettri2  24257  met0  24259  metge0  24261  metsym  24266  metrtri  24273  metgt0  24275  metres2  24279  prdsmet  24286  imasf1omet  24292  blpnf  24313  bl2in  24316  isms2  24366  setsms  24396  tmsms  24403  metss2lem  24427  metss2  24428  methaus  24436  dscopn  24489  ngpocelbl  24620  cnxmet  24688  rexmet  24707  metdcn2  24756  metdsre  24770  metdscn2  24774  lebnumlem1  24888  lebnumlem2  24889  lebnumlem3  24890  lebnum  24891  xlebnum  24892  cmetcaulem  25216  cmetcau  25217  iscmet3lem1  25219  iscmet3lem2  25220  iscmet3  25221  equivcfil  25227  equivcau  25228  metsscmetcld  25243  cmetss  25244  relcmpcmet  25246  cmpcmet  25247  cncmet  25250  bcthlem2  25253  bcthlem3  25254  bcthlem4  25255  bcthlem5  25256  bcth2  25258  bcth3  25259  cmetcusp1  25281  cmetcusp  25282  minveclem3  25357  imsxmet  30670  blocni  30783  ubthlem1  30848  ubthlem2  30849  minvecolem4a  30855  hhxmet  31153  hilxmet  31173  fmcncfil  33942  blssp  37802  lmclim2  37804  geomcau  37805  caures  37806  caushft  37807  sstotbnd2  37820  equivtotbnd  37824  isbndx  37828  isbnd3  37830  ssbnd  37834  totbndbnd  37835  prdstotbnd  37840  prdsbnd2  37841  heibor1lem  37855  heibor1  37856  heiborlem3  37859  heiborlem6  37862  heiborlem8  37864  heiborlem9  37865  heiborlem10  37866  heibor  37867  bfplem1  37868  bfplem2  37869  rrncmslem  37878  ismrer1  37884  reheibor  37885  metpsmet  45134  qndenserrnbllem  46338  qndenserrnbl  46339  qndenserrnopnlem  46341  rrndsxmet  46347  hoiqssbllem2  46667  hoiqssbl  46669  opnvonmbllem2  46677