Theorem cmetmet 25402

Description: A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 29-Jan-2014.)

Assertion

Ref	Expression
cmetmet	⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))

Proof of Theorem cmetmet

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2765	. . 3 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
2	1	iscmet 25400	. 2 ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)((MetOpen‘𝐷) fLim 𝑓) ≠ ∅))
3	2	simplbi 501	1 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))

Syntax hints:   → wi 4   ∈ wcel 2145   ≠ wne 2960  ∀wral 3079  ∅c0 4288  ‘cfv 6525  (class class class)co 7400  Metcmet 21465  MetOpencmopn 21469   fLim cflim 24048  CauFilccfil 25368  CMetccmet 25370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-cmet 25373

This theorem is referenced by:  cmetmeti  25403  cmetcaulem  25404  cmetcau  25405  iscmet2  25410  metsscmetcld  25431  cmetss  25432  bcthlem2  25441  bcthlem3  25442  bcthlem4  25443  bcthlem5  25444  bcth2  25446  bcth3  25447  cmetcusp1  25469  cmetcusp  25470  minveclem3  25545  ubthlem1  31127  ubthlem2  31128  hlmet  31152  fmcncfil  34233  heiborlem3  38319  heiborlem6  38322  heiborlem8  38324  heiborlem9  38325  heiborlem10  38326  heibor  38327  bfplem1  38328  bfplem2  38329  bfp  38330