Theorem metxmet 24289

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

Syntax hints:   → wi 4   ∈ wcel 2098   × cxp 5676  ⟶wf 6545  ‘cfv 6549  ℝcr 11144  ∞Metcxmet 21286  Metcmet 21287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-mulcl 11207  ax-i2m1 11213

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11287  df-mnf 11288  df-xr 11289  df-xadd 13133  df-xmet 21294  df-met 21295

This theorem is referenced by:  metdmdm  24291  meteq0  24294  mettri2  24296  met0  24298  metge0  24300  metsym  24305  metrtri  24312  metgt0  24314  metres2  24318  prdsmet  24325  imasf1omet  24331  blpnf  24352  bl2in  24355  isms2  24405  setsms  24437  tmsms  24445  metss2lem  24469  metss2  24470  methaus  24478  dscopn  24531  ngpocelbl  24670  cnxmet  24738  rexmet  24756  metdcn2  24804  metdsre  24818  metdscn2  24822  lebnumlem1  24936  lebnumlem2  24937  lebnumlem3  24938  lebnum  24939  xlebnum  24940  cmetcaulem  25265  cmetcau  25266  iscmet3lem1  25268  iscmet3lem2  25269  iscmet3  25270  equivcfil  25276  equivcau  25277  metsscmetcld  25292  cmetss  25293  relcmpcmet  25295  cmpcmet  25296  cncmet  25299  bcthlem2  25302  bcthlem3  25303  bcthlem4  25304  bcthlem5  25305  bcth2  25307  bcth3  25308  cmetcusp1  25330  cmetcusp  25331  minveclem3  25406  imsxmet  30579  blocni  30692  ubthlem1  30757  ubthlem2  30758  minvecolem4a  30764  hhxmet  31062  hilxmet  31082  fmcncfil  33665  blssp  37362  lmclim2  37364  geomcau  37365  caures  37366  caushft  37367  sstotbnd2  37380  equivtotbnd  37384  isbndx  37388  isbnd3  37390  ssbnd  37394  totbndbnd  37395  prdstotbnd  37400  prdsbnd2  37401  heibor1lem  37415  heibor1  37416  heiborlem3  37419  heiborlem6  37422  heiborlem8  37424  heiborlem9  37425  heiborlem10  37426  heibor  37427  bfplem1  37428  bfplem2  37429  rrncmslem  37438  ismrer1  37444  reheibor  37445  metpsmet  44599  qndenserrnbllem  45822  qndenserrnbl  45823  qndenserrnopnlem  45825  rrndsxmet  45831  hoiqssbllem2  46151  hoiqssbl  46153  opnvonmbllem2  46161