Theorem metxmet 24381

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

Syntax hints:   → wi 4   ∈ wcel 2141   × cxp 5641  ⟶wf 6511  ‘cfv 6515  ℝcr 11065  ∞Metcxmet 21396  Metcmet 21397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-mulcl 11128  ax-i2m1 11134

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8671  df-map 8803  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-xadd 13108  df-xmet 21404  df-met 21405

This theorem is referenced by:  metdmdm  24383  meteq0  24386  mettri2  24388  met0  24390  metge0  24392  metsym  24397  metrtri  24404  metgt0  24406  metres2  24410  prdsmet  24417  imasf1omet  24423  blpnf  24444  bl2in  24447  isms2  24497  setsms  24527  tmsms  24534  metss2lem  24558  metss2  24559  methaus  24567  dscopn  24620  ngpocelbl  24751  cnxmet  24819  rexmet  24838  metdcn2  24887  metdsre  24901  metdscn2  24905  lebnumlem1  25010  lebnumlem2  25011  lebnumlem3  25012  lebnum  25013  xlebnum  25014  cmetcaulem  25337  cmetcau  25338  iscmet3lem1  25340  iscmet3lem2  25341  iscmet3  25342  equivcfil  25348  equivcau  25349  metsscmetcld  25364  cmetss  25365  relcmpcmet  25367  cmpcmet  25368  cncmet  25371  bcthlem2  25374  bcthlem3  25375  bcthlem4  25376  bcthlem5  25377  bcth2  25379  bcth3  25380  cmetcusp1  25402  cmetcusp  25403  minveclem3  25478  imsxmet  30851  blocni  30964  ubthlem1  31029  ubthlem2  31030  minvecolem4a  31036  hhxmet  31334  hilxmet  31354  fmcncfil  34188  blssp  38215  lmclim2  38217  geomcau  38218  caures  38219  caushft  38220  sstotbnd2  38233  equivtotbnd  38237  isbndx  38241  isbnd3  38243  ssbnd  38247  totbndbnd  38248  prdstotbnd  38253  prdsbnd2  38254  heibor1lem  38268  heibor1  38269  heiborlem3  38272  heiborlem6  38275  heiborlem8  38277  heiborlem9  38278  heiborlem10  38279  heibor  38280  bfplem1  38281  bfplem2  38282  rrncmslem  38291  ismrer1  38297  reheibor  38298  metpsmet  45629  qndenserrnbllem  46828  qndenserrnbl  46829  qndenserrnopnlem  46831  rrndsxmet  46837  hoiqssbllem2  47157  hoiqssbl  47159  opnvonmbllem2  47167