![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cmetmet | Structured version Visualization version GIF version |
Description: A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 29-Jan-2014.) |
Ref | Expression |
---|---|
cmetmet | ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2732 | . . 3 ⊢ (MetOpen‘𝐷) = (MetOpen‘𝐷) | |
2 | 1 | iscmet 24792 | . 2 ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)((MetOpen‘𝐷) fLim 𝑓) ≠ ∅)) |
3 | 2 | simplbi 498 | 1 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∅c0 4321 ‘cfv 6540 (class class class)co 7405 Metcmet 20922 MetOpencmopn 20926 fLim cflim 23429 CauFilccfil 24760 CMetccmet 24762 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-iota 6492 df-fun 6542 df-fv 6548 df-ov 7408 df-cmet 24765 |
This theorem is referenced by: cmetmeti 24795 cmetcaulem 24796 cmetcau 24797 iscmet2 24802 metsscmetcld 24823 cmetss 24824 bcthlem2 24833 bcthlem3 24834 bcthlem4 24835 bcthlem5 24836 bcth2 24838 bcth3 24839 cmetcusp1 24861 cmetcusp 24862 minveclem3 24937 ubthlem1 30110 ubthlem2 30111 hlmet 30135 fmcncfil 32899 heiborlem3 36669 heiborlem6 36672 heiborlem8 36674 heiborlem9 36675 heiborlem10 36676 heibor 36677 bfplem1 36678 bfplem2 36679 bfp 36680 |
Copyright terms: Public domain | W3C validator |