Theorem metxmet 24060

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

Syntax hints:   → wi 4   ∈ wcel 2104   × cxp 5673  ⟶wf 6538  ‘cfv 6542  ℝcr 11111  ∞Metcxmet 21129  Metcmet 21130

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-mulcl 11174  ax-i2m1 11180

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-xadd 13097  df-xmet 21137  df-met 21138

This theorem is referenced by:  metdmdm  24062  meteq0  24065  mettri2  24067  met0  24069  metge0  24071  metsym  24076  metrtri  24083  metgt0  24085  metres2  24089  prdsmet  24096  imasf1omet  24102  blpnf  24123  bl2in  24126  isms2  24176  setsms  24208  tmsms  24216  metss2lem  24240  metss2  24241  methaus  24249  dscopn  24302  ngpocelbl  24441  cnxmet  24509  rexmet  24527  metdcn2  24575  metdsre  24589  metdscn2  24593  lebnumlem1  24707  lebnumlem2  24708  lebnumlem3  24709  lebnum  24710  xlebnum  24711  cmetcaulem  25036  cmetcau  25037  iscmet3lem1  25039  iscmet3lem2  25040  iscmet3  25041  equivcfil  25047  equivcau  25048  metsscmetcld  25063  cmetss  25064  relcmpcmet  25066  cmpcmet  25067  cncmet  25070  bcthlem2  25073  bcthlem3  25074  bcthlem4  25075  bcthlem5  25076  bcth2  25078  bcth3  25079  cmetcusp1  25101  cmetcusp  25102  minveclem3  25177  imsxmet  30212  blocni  30325  ubthlem1  30390  ubthlem2  30391  minvecolem4a  30397  hhxmet  30695  hilxmet  30715  fmcncfil  33209  blssp  36927  lmclim2  36929  geomcau  36930  caures  36931  caushft  36932  sstotbnd2  36945  equivtotbnd  36949  isbndx  36953  isbnd3  36955  ssbnd  36959  totbndbnd  36960  prdstotbnd  36965  prdsbnd2  36966  heibor1lem  36980  heibor1  36981  heiborlem3  36984  heiborlem6  36987  heiborlem8  36989  heiborlem9  36990  heiborlem10  36991  heibor  36992  bfplem1  36993  bfplem2  36994  rrncmslem  37003  ismrer1  37009  reheibor  37010  metpsmet  44081  qndenserrnbllem  45308  qndenserrnbl  45309  qndenserrnopnlem  45311  rrndsxmet  45317  hoiqssbllem2  45637  hoiqssbl  45639  opnvonmbllem2  45647