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

Metamath Proof Explorer

Definition df-cms

Description: Define the class of complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion df-cms CMetSp = { 𝑤 ∈ MetSp ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccms ⊢ CMetSp
1 vw ⊢ 𝑤
2 cms ⊢ MetSp
3 cbs ⊢ Base
4 1 cv ⊢ 𝑤
5 4 3 cfv ⊢ ( Base ‘ 𝑤 )
6 vb ⊢ 𝑏
7 cds ⊢ dist
8 4 7 cfv ⊢ ( dist ‘ 𝑤 )
9 6 cv ⊢ 𝑏
10 9 9 cxp ⊢ ( 𝑏 × 𝑏 )
11 8 10 cres ⊢ ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) )
12 ccmet ⊢ CMet
13 9 12 cfv ⊢ ( CMet ‘ 𝑏 )
14 11 13 wcel ⊢ ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 )
15 14 6 5 wsbc ⊢ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 )
16 15 1 2 crab ⊢ { 𝑤 ∈ MetSp ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) }
17 0 16 wceq ⊢ CMetSp = { 𝑤 ∈ MetSp ∣ [ ( Base ‘ 𝑤 ) / 𝑏 ] ( ( dist ‘ 𝑤 ) ↾ ( 𝑏 × 𝑏 ) ) ∈ ( CMet ‘ 𝑏 ) }