This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
relcmpcmet.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
cmpcmet.3 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
Assertion cmpcmet ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 relcmpcmet.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 relcmpcmet.2 ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
3 cmpcmet.3 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
4 1rp ⊢ 1 ∈ ℝ+
5 4 a1i ⊢ ( 𝜑 → 1 ∈ ℝ+ )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ Comp )
7 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
8 2 7 syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
10 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
11 9 10 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ Top )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
13 rpxr ⊢ ( 1 ∈ ℝ+ → 1 ∈ ℝ* )
14 4 13 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 1 ∈ ℝ* )
15 blssm ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ* ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 )
16 9 12 14 15 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ 𝑋 )
17 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
18 9 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑋 = ∪ 𝐽 )
19 16 18 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ ∪ 𝐽 )
20 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
21 20 clscld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ∈ ( Clsd ‘ 𝐽 ) )
22 11 19 21 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ∈ ( Clsd ‘ 𝐽 ) )
23 cmpcld ⊢ ( ( 𝐽 ∈ Comp ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) ∈ Comp )
24 6 22 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ ( 𝑥 ( ball ‘ 𝐷 ) 1 ) ) ) ∈ Comp )
25 1 2 5 24 relcmpcmet ⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )