Metamath Proof Explorer

Theorem cmetcau

Description: The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 14-Oct-2015)

Ref Expression
Hypothesis cmetcau.1 
|- J = ( MetOpen ` D )
Assertion cmetcau 
|- ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) -> F e. dom ( ~~>t ` J ) )

Proof

Step Hyp Ref Expression
1 cmetcau.1 
 |-  J = ( MetOpen ` D )
2 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
3 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
4 2 3 syl 
 |-  ( D e. ( CMet ` X ) -> D e. ( *Met ` X ) )
5 caun0 
 |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> X =/= (/) )
6 4 5 sylan 
 |-  ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) -> X =/= (/) )
7 n0 
 |-  ( X =/= (/) <-> E. x x e. X )
8 6 7 sylib 
 |-  ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) -> E. x x e. X )
9 simpll 
 |-  ( ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) /\ x e. X ) -> D e. ( CMet ` X ) )
10 simpr 
 |-  ( ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) /\ x e. X ) -> x e. X )
11 simplr 
 |-  ( ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) /\ x e. X ) -> F e. ( Cau ` D ) )
12 eqid 
 |-  ( y e. NN |-> if ( y e. dom F , ( F ` y ) , x ) ) = ( y e. NN |-> if ( y e. dom F , ( F ` y ) , x ) )
13 1 9 10 11 12 cmetcaulem 
 |-  ( ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) /\ x e. X ) -> F e. dom ( ~~>t ` J ) )
14 8 13 exlimddv 
 |-  ( ( D e. ( CMet ` X ) /\ F e. ( Cau ` D ) ) -> F e. dom ( ~~>t ` J ) )