Theorem metxmet 24633

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   × cxp 5649  ⟶wf 6527  ‘cfv 6531  ℝcr 11180  ∞Metcxmet 21643  Metcmet 21644

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740  ax-cnex 11237  ax-resscn 11238  ax-1cn 11239  ax-icn 11240  ax-addcl 11241  ax-mulcl 11243  ax-i2m1 11249

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-er 8701  df-map 8833  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11326  df-mnf 11327  df-xr 11328  df-xadd 13223  df-xmet 21651  df-met 21652

This theorem is used by:  metdmdm  24635  meteq0  24638  mettri2  24640  met0  24642  metge0  24644  metsym  24649  metrtri  24656  metgt0  24658  metres2  24662  prdsmet  24669  imasf1omet  24675  blpnf  24696  bl2in  24699  isms2  24749  setsms  24779  tmsms  24786  metss2lem  24810  metss2  24811  methaus  24819  dscopn  24872  ngpocelbl  25003  cnxmet  25071  rexmet  25090  metdcn2  25139  metdsre  25153  metdscn2  25157  lebnumlem1  25262  lebnumlem2  25263  lebnumlem3  25264  lebnum  25265  xlebnum  25266  cmetcaulem  25589  cmetcau  25590  iscmet3lem1  25592  iscmet3lem2  25593  iscmet3  25594  equivcfil  25600  equivcau  25601  metsscmetcld  25616  cmetss  25617  relcmpcmet  25619  cmpcmet  25620  cncmet  25623  bcthlem2  25626  bcthlem3  25627  bcthlem4  25628  bcthlem5  25629  bcth2  25631  bcth3  25632  cmetcusp1  25654  cmetcusp  25655  minveclem3  25730  imsxmet  31276  blocni  31389  ubthlem1  31454  ubthlem2  31455  minvecolem4a  31461  hhxmet  31759  hilxmet  31779  fmcncfil  34545  blssp  38658  lmclim2  38660  geomcau  38661  caures  38662  caushft  38663  sstotbnd2  38676  equivtotbnd  38680  isbndx  38684  isbnd3  38686  ssbnd  38690  totbndbnd  38691  prdstotbnd  38696  prdsbnd2  38697  heibor1lem  38711  heibor1  38712  heiborlem3  38715  heiborlem6  38718  heiborlem8  38720  heiborlem9  38721  heiborlem10  38722  heibor  38723  bfplem1  38724  bfplem2  38725  rrncmslem  38734  ismrer1  38740  reheibor  38741  metpsmet  46049  qndenserrnbllem  47248  qndenserrnbl  47249  qndenserrnopnlem  47251  rrndsxmet  47257  hoiqssbllem2  47577  hoiqssbl  47579  opnvonmbllem2  47587