Metamath Proof Explorer

Theorem cmpcmet

Description: A compact metric space is complete. One half of heibor . (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses relcmpcmet.1 ⊢J=MetOpen⁡D
relcmpcmet.2 ⊢φ→D∈Met⁡X
cmpcmet.3 ⊢φ→J∈Comp
Assertion cmpcmet ⊢φ→D∈CMet⁡X

Proof

Step Hyp Ref Expression
1 relcmpcmet.1 ⊢J=MetOpen⁡D
2 relcmpcmet.2 ⊢φ→D∈Met⁡X
3 cmpcmet.3 ⊢φ→J∈Comp
4 1rp ⊢1∈ℝ+
5 4 a1i ⊢φ→1∈ℝ+
6 3 adantr ⊢φ∧x∈X→J∈Comp
7 metxmet ⊢D∈Met⁡X→D∈∞Met⁡X
8 2 7 syl ⊢φ→D∈∞Met⁡X
9 8 adantr ⊢φ∧x∈X→D∈∞Met⁡X
10 1 mopntop ⊢D∈∞Met⁡X→J∈Top
11 9 10 syl ⊢φ∧x∈X→J∈Top
12 simpr ⊢φ∧x∈X→x∈X
13 rpxr ⊢1∈ℝ+→1∈ℝ*
14 4 13 mp1i ⊢φ∧x∈X→1∈ℝ*
15 blssm ⊢D∈∞Met⁡X∧x∈X∧1∈ℝ*→xball⁡D1⊆X
16 9 12 14 15 syl3anc ⊢φ∧x∈X→xball⁡D1⊆X
17 1 mopnuni ⊢D∈∞Met⁡X→X=⋃J
18 9 17 syl ⊢φ∧x∈X→X=⋃J
19 16 18 sseqtrd ⊢φ∧x∈X→xball⁡D1⊆⋃J
20 eqid ⊢⋃J=⋃J
21 20 clscld ⊢J∈Top∧xball⁡D1⊆⋃J→cls⁡J⁡xball⁡D1∈Clsd⁡J
22 11 19 21 syl2anc ⊢φ∧x∈X→cls⁡J⁡xball⁡D1∈Clsd⁡J
23 cmpcld ⊢J∈Comp∧cls⁡J⁡xball⁡D1∈Clsd⁡J→J↾𝑡cls⁡J⁡xball⁡D1∈Comp
24 6 22 23 syl2anc ⊢φ∧x∈X→J↾𝑡cls⁡J⁡xball⁡D1∈Comp
25 1 2 5 24 relcmpcmet ⊢φ→D∈CMet⁡X