Metamath Proof Explorer

Theorem iscmet

Description: The property " D is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014) (Revised by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypothesis iscmet.1 
|- J = ( MetOpen ` D )
Assertion iscmet 
|- ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 iscmet.1 
 |-  J = ( MetOpen ` D )
2 elfvex 
 |-  ( D e. ( CMet ` X ) -> X e. _V )
3 elfvex 
 |-  ( D e. ( Met ` X ) -> X e. _V )
4 3 adantr 
 |-  ( ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) -> X e. _V )
5 fveq2 
 |-  ( x = X -> ( Met ` x ) = ( Met ` X ) )
6 5 rabeqdv 
 |-  ( x = X -> { d e. ( Met ` x ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } = { d e. ( Met ` X ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )
7 df-cmet 
 |-  CMet = ( x e. _V |-> { d e. ( Met ` x ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )
8 fvex 
 |-  ( Met ` X ) e. _V
9 8 rabex 
 |-  { d e. ( Met ` X ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } e. _V
10 6 7 9 fvmpt 
 |-  ( X e. _V -> ( CMet ` X ) = { d e. ( Met ` X ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } )
11 10 eleq2d 
 |-  ( X e. _V -> ( D e. ( CMet ` X ) <-> D e. { d e. ( Met ` X ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } ) )
12 fveq2 
 |-  ( d = D -> ( CauFil ` d ) = ( CauFil ` D ) )
13 fveq2 
 |-  ( d = D -> ( MetOpen ` d ) = ( MetOpen ` D ) )
14 13 1 eqtr4di 
 |-  ( d = D -> ( MetOpen ` d ) = J )
15 14 oveq1d 
 |-  ( d = D -> ( ( MetOpen ` d ) fLim f ) = ( J fLim f ) )
16 15 neeq1d 
 |-  ( d = D -> ( ( ( MetOpen ` d ) fLim f ) =/= (/) <-> ( J fLim f ) =/= (/) ) )
17 12 16 raleqbidv 
 |-  ( d = D -> ( A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) <-> A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) )
18 17 elrab 
 |-  ( D e. { d e. ( Met ` X ) | A. f e. ( CauFil ` d ) ( ( MetOpen ` d ) fLim f ) =/= (/) } <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) )
19 11 18 bitrdi 
 |-  ( X e. _V -> ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) ) )
20 2 4 19 pm5.21nii 
 |-  ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ A. f e. ( CauFil ` D ) ( J fLim f ) =/= (/) ) )