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	|- ( ph -> D e. ( Met ` X ) )
	cmpcmet.3	|- ( ph -> J e. Comp )
Assertion	cmpcmet	|- ( ph -> D e. ( CMet ` X ) )

Proof

Step	Hyp	Ref	Expression
1		relcmpcmet.1	|- J = ( MetOpen ` D )
2		relcmpcmet.2	|- ( ph -> D e. ( Met ` X ) )
3		cmpcmet.3	|- ( ph -> J e. Comp )
4		1rp	|- 1 e. RR+
5	4	a1i	|- ( ph -> 1 e. RR+ )
6	3	adantr	|- ( ( ph /\ x e. X ) -> J e. Comp )
7		metxmet	|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
8	2 7	syl	|- ( ph -> D e. ( *Met ` X ) )
9	8	adantr	|- ( ( ph /\ x e. X ) -> D e. ( *Met ` X ) )
10	1	mopntop	|- ( D e. ( *Met ` X ) -> J e. Top )
11	9 10	syl	|- ( ( ph /\ x e. X ) -> J e. Top )
12		simpr	|- ( ( ph /\ x e. X ) -> x e. X )
13		rpxr	|- ( 1 e. RR+ -> 1 e. RR* )
14	4 13	mp1i	|- ( ( ph /\ x e. X ) -> 1 e. RR* )
15		blssm	|- ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) C_ X )
16	9 12 14 15	syl3anc	|- ( ( ph /\ x e. X ) -> ( x ( ball ` D ) 1 ) C_ X )
17	1	mopnuni	|- ( D e. ( *Met ` X ) -> X = U. J )
18	9 17	syl	|- ( ( ph /\ x e. X ) -> X = U. J )
19	16 18	sseqtrd	|- ( ( ph /\ x e. X ) -> ( x ( ball ` D ) 1 ) C_ U. J )
20		eqid	|- U. J = U. J
21	20	clscld	|- ( ( J e. Top /\ ( x ( ball ` D ) 1 ) C_ U. J ) -> ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` J ) )
22	11 19 21	syl2anc	|- ( ( ph /\ x e. X ) -> ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` J ) )
23		cmpcld	|- ( ( J e. Comp /\ ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` J ) ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp )
24	6 22 23	syl2anc	|- ( ( ph /\ x e. X ) -> ( J |`t ( ( cls ` J ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp )
25	1 2 5 24	relcmpcmet	|- ( ph -> D e. ( CMet ` X ) )