Theorem iscms

Description: A complete metric space is a metric space with a complete metric. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	iscms.1	⊢ 𝑋 = ( Base ‘ 𝑀 )
	iscms.2	⊢ 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
Assertion	iscms	⊢ ( 𝑀 ∈ CMetSp ↔ ( 𝑀 ∈ MetSp ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscms.1	⊢ 𝑋 = ( Base ‘ 𝑀 )
2		iscms.2	⊢ 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
3		fvexd	⊢ ( 𝑤 = 𝑀 → ( Base ‘ 𝑤 ) ∈ V )
4		fveq2	⊢ ( 𝑤 = 𝑀 → ( dist ‘ 𝑤 ) = ( dist ‘ 𝑀 ) )
5	4	adantr	⊢ ( ( 𝑤 = 𝑀 ∧ 𝑏 = ( Base ‘ 𝑤 ) ) → ( dist ‘ 𝑤 ) = ( dist ‘ 𝑀 ) )
6		id	⊢ ( 𝑏 = ( Base ‘ 𝑤 ) → 𝑏 = ( Base ‘ 𝑤 ) )
7		fveq2	⊢ ( 𝑤 = 𝑀 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑀 ) )
8	7 1	eqtr4di	⊢ ( 𝑤 = 𝑀 → ( Base ‘ 𝑤 ) = 𝑋 )
9	6 8	sylan9eqr	⊢ ( ( 𝑤 = 𝑀 ∧ 𝑏 = ( Base ‘ 𝑤 ) ) → 𝑏 = 𝑋 )
10	9	sqxpeqd	⊢ ( ( 𝑤 = 𝑀 ∧ 𝑏 = ( Base ‘ 𝑤 ) ) → ( 𝑏 × 𝑏 ) = ( 𝑋 × 𝑋 ) )
11	5 10	reseq12d	⊢ ( ( 𝑤 = 𝑀 ∧ 𝑏 = ( Base ‘ 𝑤 ) ) → ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
12	11 2	eqtr4di	⊢ ( ( 𝑤 = 𝑀 ∧ 𝑏 = ( Base ‘ 𝑤 ) ) → ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) = 𝐷 )
13	9	fveq2d	⊢ ( ( 𝑤 = 𝑀 ∧ 𝑏 = ( Base ‘ 𝑤 ) ) → ( CMet ‘ 𝑏 ) = ( CMet ‘ 𝑋 ) )
14	12 13	eleq12d	⊢ ( ( 𝑤 = 𝑀 ∧ 𝑏 = ( Base ‘ 𝑤 ) ) → ( ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) ↔ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )
15	3 14	sbcied	⊢ ( 𝑤 = 𝑀 → ( [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) ↔ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )
16		df-cms	⊢ CMetSp = { 𝑤 ∈ MetSp ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) }
17	15 16	elrab2	⊢ ( 𝑀 ∈ CMetSp ↔ ( 𝑀 ∈ MetSp ∧ 𝐷 ∈ ( CMet ‘ 𝑋 ) ) )