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

Metamath Proof Explorer

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