Theorem metxmet 21886

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

Syntax hints:   → wi 4   ∈ wcel 1975   × cxp 5022  ⟶wf 5782  ‘cfv 5786  ℝcr 9787  ∞Metcxmt 19494  Metcme 19495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-mulcl 9850  ax-i2m1 9856

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-mpt 4635  df-id 4939  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-er 7602  df-map 7719  df-en 7815  df-dom 7816  df-sdom 7817  df-pnf 9928  df-mnf 9929  df-xr 9930  df-xadd 11775  df-xmet 19502  df-met 19503

This theorem is referenced by:  metdmdm  21888  meteq0  21891  mettri2  21893  met0  21895  metge0  21897  metsym  21902  metrtri  21909  metgt0  21911  metres2  21915  prdsmet  21922  imasf1omet  21928  blpnf  21949  bl2in  21952  isms2  22002  setsms  22032  tmsms  22039  metss2lem  22063  metss2  22064  methaus  22072  dscopn  22125  cnxmet  22314  rexmet  22330  metdcn2  22378  metdsre  22391  metdscn2  22395  lebnumlem1  22495  lebnumlem2  22496  lebnumlem3  22497  lebnum  22498  xlebnum  22499  cmetcaulem  22808  cmetcau  22809  iscmet3lem1  22811  iscmet3lem2  22812  iscmet3  22813  equivcfil  22819  equivcau  22820  cmetss  22834  relcmpcmet  22836  cmpcmet  22837  cncmet  22840  bcthlem2  22843  bcthlem3  22844  bcthlem4  22845  bcthlem5  22846  bcth2  22848  bcth3  22849  cmetcusp1  22870  cmetcusp  22871  minveclem3  22921  imsxmet  26724  blocni  26846  ubthlem1  26912  ubthlem2  26913  minvecolem4a  26919  hhxmet  27218  hilxmet  27238  fmcncfil  29107  blssp  32521  lmclim2  32523  geomcau  32524  caures  32525  caushft  32526  sstotbnd2  32542  equivtotbnd  32546  isbndx  32550  isbnd3  32552  ssbnd  32556  totbndbnd  32557  prdstotbnd  32562  prdsbnd2  32563  heibor1lem  32577  heibor1  32578  heiborlem3  32581  heiborlem6  32584  heiborlem8  32586  heiborlem9  32587  heiborlem10  32588  heibor  32589  bfplem1  32590  bfplem2  32591  rrncmslem  32600  ismrer1  32606  reheibor  32607  metpsmet  38095  qndenserrnbllem  38990  qndenserrnbl  38991  qndenserrnopnlem  38993  rrndsxmet  38999  hoiqssbllem2  39313  hoiqssbl  39315  opnvonmbllem2  39323