Theorem metxmet 24238

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

Syntax hints:   → wi 4   ∈ wcel 2109   × cxp 5621  ⟶wf 6482  ‘cfv 6486  ℝcr 11027  ∞Metcxmet 21264  Metcmet 21265

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-i2m1 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-map 8762  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-xadd 13033  df-xmet 21272  df-met 21273

This theorem is referenced by:  metdmdm  24240  meteq0  24243  mettri2  24245  met0  24247  metge0  24249  metsym  24254  metrtri  24261  metgt0  24263  metres2  24267  prdsmet  24274  imasf1omet  24280  blpnf  24301  bl2in  24304  isms2  24354  setsms  24384  tmsms  24391  metss2lem  24415  metss2  24416  methaus  24424  dscopn  24477  ngpocelbl  24608  cnxmet  24676  rexmet  24695  metdcn2  24744  metdsre  24758  metdscn2  24762  lebnumlem1  24876  lebnumlem2  24877  lebnumlem3  24878  lebnum  24879  xlebnum  24880  cmetcaulem  25204  cmetcau  25205  iscmet3lem1  25207  iscmet3lem2  25208  iscmet3  25209  equivcfil  25215  equivcau  25216  metsscmetcld  25231  cmetss  25232  relcmpcmet  25234  cmpcmet  25235  cncmet  25238  bcthlem2  25241  bcthlem3  25242  bcthlem4  25243  bcthlem5  25244  bcth2  25246  bcth3  25247  cmetcusp1  25269  cmetcusp  25270  minveclem3  25345  imsxmet  30654  blocni  30767  ubthlem1  30832  ubthlem2  30833  minvecolem4a  30839  hhxmet  31137  hilxmet  31157  fmcncfil  33897  blssp  37735  lmclim2  37737  geomcau  37738  caures  37739  caushft  37740  sstotbnd2  37753  equivtotbnd  37757  isbndx  37761  isbnd3  37763  ssbnd  37767  totbndbnd  37768  prdstotbnd  37773  prdsbnd2  37774  heibor1lem  37788  heibor1  37789  heiborlem3  37792  heiborlem6  37795  heiborlem8  37797  heiborlem9  37798  heiborlem10  37799  heibor  37800  bfplem1  37801  bfplem2  37802  rrncmslem  37811  ismrer1  37817  reheibor  37818  metpsmet  45069  qndenserrnbllem  46276  qndenserrnbl  46277  qndenserrnopnlem  46279  rrndsxmet  46285  hoiqssbllem2  46605  hoiqssbl  46607  opnvonmbllem2  46615