Theorem cmetmet 25640

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 2763	. . 3 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷)
2	1	iscmet 25638	. 2 ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)((MetOpen‘𝐷) fLim 𝑓) ≠ ∅))
3	2	simplbi 502	1 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∅c0 4281  ‘cfv 6561  (class class class)co 7446  Metcmet 21697  MetOpencmopn 21701   fLim cflim 24286  CauFilccfil 25606  CMetccmet 25608

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-iota 6515  df-fun 6563  df-fv 6569  df-ov 7449  df-cmet 25611

This theorem is used by:  cmetmeti  25641  cmetcaulem  25642  cmetcau  25643  iscmet2  25648  metsscmetcld  25669  cmetss  25670  bcthlem2  25679  bcthlem3  25680  bcthlem4  25681  bcthlem5  25682  bcth2  25684  bcth3  25685  cmetcusp1  25707  cmetcusp  25708  minveclem3  25783  ubthlem1  31505  ubthlem2  31506  hlmet  31530  fmcncfil  34646  heiborlem3  38950  heiborlem6  38953  heiborlem8  38955  heiborlem9  38956  heiborlem10  38957  heibor  38958  bfplem1  38959  bfplem2  38960  bfp  38961