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 ‘ 𝑋 ) )