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 ∈ ℝ * → x ball ⁡ D 1 ⊆ X
16 9 12 14 15 syl3anc ⊢ φ ∧ x ∈ X → x ball ⁡ D 1 ⊆ X
17 1 mopnuni ⊢ D ∈ ∞Met ⁡ X → X = ⋃ J
18 9 17 syl ⊢ φ ∧ x ∈ X → X = ⋃ J
19 16 18 sseqtrd ⊢ φ ∧ x ∈ X → x ball ⁡ D 1 ⊆ ⋃ J
20 eqid ⊢ ⋃ J = ⋃ J
21 20 clscld ⊢ J ∈ Top ∧ x ball ⁡ D 1 ⊆ ⋃ J → cls ⁡ J ⁡ x ball ⁡ D 1 ∈ Clsd ⁡ J
22 11 19 21 syl2anc ⊢ φ ∧ x ∈ X → cls ⁡ J ⁡ x ball ⁡ D 1 ∈ Clsd ⁡ J
23 cmpcld ⊢ J ∈ Comp ∧ cls ⁡ J ⁡ x ball ⁡ D 1 ∈ Clsd ⁡ J → J ↾ 𝑡 cls ⁡ J ⁡ x ball ⁡ D 1 ∈ Comp
24 6 22 23 syl2anc ⊢ φ ∧ x ∈ X → J ↾ 𝑡 cls ⁡ J ⁡ x ball ⁡ D 1 ∈ Comp
25 1 2 5 24 relcmpcmet ⊢ φ → D ∈ CMet ⁡ X