Theorem metxmet 24324

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

Syntax hints:   → wi 4   ∈ wcel 2119   × cxp 5623  ⟶wf 6488  ‘cfv 6492  ℝcr 11035  ∞Metcxmet 21339  Metcmet 21340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-mulcl 11098  ax-i2m1 11104

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-er 8640  df-map 8772  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-xadd 13062  df-xmet 21347  df-met 21348

This theorem is referenced by:  metdmdm  24326  meteq0  24329  mettri2  24331  met0  24333  metge0  24335  metsym  24340  metrtri  24347  metgt0  24349  metres2  24353  prdsmet  24360  imasf1omet  24366  blpnf  24387  bl2in  24390  isms2  24440  setsms  24470  tmsms  24477  metss2lem  24501  metss2  24502  methaus  24510  dscopn  24563  ngpocelbl  24694  cnxmet  24762  rexmet  24781  metdcn2  24830  metdsre  24844  metdscn2  24848  lebnumlem1  24953  lebnumlem2  24954  lebnumlem3  24955  lebnum  24956  xlebnum  24957  cmetcaulem  25280  cmetcau  25281  iscmet3lem1  25283  iscmet3lem2  25284  iscmet3  25285  equivcfil  25291  equivcau  25292  metsscmetcld  25307  cmetss  25308  relcmpcmet  25310  cmpcmet  25311  cncmet  25314  bcthlem2  25317  bcthlem3  25318  bcthlem4  25319  bcthlem5  25320  bcth2  25322  bcth3  25323  cmetcusp1  25345  cmetcusp  25346  minveclem3  25421  imsxmet  30788  blocni  30901  ubthlem1  30966  ubthlem2  30967  minvecolem4a  30973  hhxmet  31271  hilxmet  31291  fmcncfil  34122  blssp  38130  lmclim2  38132  geomcau  38133  caures  38134  caushft  38135  sstotbnd2  38148  equivtotbnd  38152  isbndx  38156  isbnd3  38158  ssbnd  38162  totbndbnd  38163  prdstotbnd  38168  prdsbnd2  38169  heibor1lem  38183  heibor1  38184  heiborlem3  38187  heiborlem6  38190  heiborlem8  38192  heiborlem9  38193  heiborlem10  38194  heibor  38195  bfplem1  38196  bfplem2  38197  rrncmslem  38206  ismrer1  38212  reheibor  38213  metpsmet  45545  qndenserrnbllem  46744  qndenserrnbl  46745  qndenserrnopnlem  46747  rrndsxmet  46753  hoiqssbllem2  47073  hoiqssbl  47075  opnvonmbllem2  47083