Theorem cmetmet 25320

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∅c0 4333  ‘cfv 6561  (class class class)co 7431  Metcmet 21350  MetOpencmopn 21354   fLim cflim 23942  CauFilccfil 25286  CMetccmet 25288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-cmet 25291

This theorem is referenced by:  cmetmeti  25321  cmetcaulem  25322  cmetcau  25323  iscmet2  25328  metsscmetcld  25349  cmetss  25350  bcthlem2  25359  bcthlem3  25360  bcthlem4  25361  bcthlem5  25362  bcth2  25364  bcth3  25365  cmetcusp1  25387  cmetcusp  25388  minveclem3  25463  ubthlem1  30889  ubthlem2  30890  hlmet  30914  fmcncfil  33930  heiborlem3  37820  heiborlem6  37823  heiborlem8  37825  heiborlem9  37826  heiborlem10  37827  heibor  37828  bfplem1  37829  bfplem2  37830  bfp  37831