Metamath Proof Explorer

Definition df-ms

Description: Define the (proper) class of metric spaces. (Contributed by NM, 27-Aug-2006)

Ref Expression
Assertion df-ms 
|- MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cms 
 |-  MetSp
1 vf 
 |-  f
2 cxms 
 |-  *MetSp
3 cds 
 |-  dist
4 1 cv 
 |-  f
5 4 3 cfv 
 |-  ( dist ` f )
6 cbs 
 |-  Base
7 4 6 cfv 
 |-  ( Base ` f )
8 7 7 cxp 
 |-  ( ( Base ` f ) X. ( Base ` f ) )
9 5 8 cres 
 |-  ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) )
10 cmet 
 |-  Met
11 7 10 cfv 
 |-  ( Met ` ( Base ` f ) )
12 9 11 wcel 
 |-  ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) )
13 12 1 2 crab 
 |-  { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }
14 0 13 wceq 
 |-  MetSp = { f e. *MetSp | ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) e. ( Met ` ( Base ` f ) ) }