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 = w ∈ MetSp | [˙Base w / b]˙ dist ⁡ w ↾ b × b ∈ CMet ⁡ b

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccms class CMetSp
1 vw setvar w
2 cms class MetSp
3 cbs class Base
4 1 cv setvar w
5 4 3 cfv class Base w
6 vb setvar b
7 cds class dist
8 4 7 cfv class dist ⁡ w
9 6 cv setvar b
10 9 9 cxp class b × b
11 8 10 cres class dist ⁡ w ↾ b × b
12 ccmet class CMet
13 9 12 cfv class CMet ⁡ b
14 11 13 wcel wff dist ⁡ w ↾ b × b ∈ CMet ⁡ b
15 14 6 5 wsbc wff [˙Base w / b]˙ dist ⁡ w ↾ b × b ∈ CMet ⁡ b
16 15 1 2 crab class w ∈ MetSp | [˙Base w / b]˙ dist ⁡ w ↾ b × b ∈ CMet ⁡ b
17 0 16 wceq wff CMetSp = w ∈ MetSp | [˙Base w / b]˙ dist ⁡ w ↾ b × b ∈ CMet ⁡ b