Metamath Proof Explorer

Definition df-xms

Description: Define the (proper) class of extended metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion df-xms 
|- *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cxms 
 |-  *MetSp
1 vf 
 |-  f
2 ctps 
 |-  TopSp
3 ctopn 
 |-  TopOpen
4 1 cv 
 |-  f
5 4 3 cfv 
 |-  ( TopOpen ` f )
6 cmopn 
 |-  MetOpen
7 cds 
 |-  dist
8 4 7 cfv 
 |-  ( dist ` f )
9 cbs 
 |-  Base
10 4 9 cfv 
 |-  ( Base ` f )
11 10 10 cxp 
 |-  ( ( Base ` f ) X. ( Base ` f ) )
12 8 11 cres 
 |-  ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) )
13 12 6 cfv 
 |-  ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) )
14 5 13 wceq 
 |-  ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) )
15 14 1 2 crab 
 |-  { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }
16 0 15 wceq 
 |-  *MetSp = { f e. TopSp | ( TopOpen ` f ) = ( MetOpen ` ( ( dist ` f ) |` ( ( Base ` f ) X. ( Base ` f ) ) ) ) }