Metamath Proof Explorer

Definition df-cmet

Description: Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014)

Ref Expression
Assertion df-cmet 
|- CMet = ( x e. _V |-> { d e. ( Met ` x ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmet 
 |-  CMet
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vd 
 |-  d
4 cmet 
 |-  Met
5 1 cv 
 |-  x
6 5 4 cfv 
 |-  ( Met ` x )
7 vf 
 |-  f
8 ccfil 
 |-  CauFil
9 3 cv 
 |-  d
10 9 8 cfv 
 |-  ( CauFil ` d )
11 cmopn 
 |-  MetOpen
12 9 11 cfv 
 |-  ( MetOpen ` d )
13 cflim 
 |-  fLim
14 7 cv 
 |-  f
15 12 14 13 co 
 |-  ( ( MetOpen ` d ) fLim f )
16 c0 
 |-  (/)
17 15 16 wne 
 |-  ( ( MetOpen ` d ) fLim f ) =/= (/)
18 17 7 10 wral 
 |-  A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/)
19 18 3 6 crab 
 |-  { d e. ( Met ` x ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) }
20 1 2 19 cmpt 
 |-  ( x e. _V |-> { d e. ( Met ` x ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )
21 0 20 wceq 
 |-  CMet = ( x e. _V |-> { d e. ( Met ` x ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )