This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iscmet2

Description: A metric D is complete iff all Cauchy sequences converge to a point in the space. The proof uses countable choice. Part of Definition 1.4-3 of Kreyszig p. 28. (Contributed by NM, 7-Sep-2006) (Revised by Mario Carneiro, 15-Oct-2015)

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

Proof

Step Hyp Ref Expression
1 iscmet2.1 
 |-  J = ( MetOpen ` D )
2 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
3 1 cmetcau 
 |-  ( ( D e. ( CMet ` X ) /\ f e. ( Cau ` D ) ) -> f e. dom ( ~~>t ` J ) )
4 3 ex 
 |-  ( D e. ( CMet ` X ) -> ( f e. ( Cau ` D ) -> f e. dom ( ~~>t ` J ) ) )
5 4 ssrdv 
 |-  ( D e. ( CMet ` X ) -> ( Cau ` D ) C_ dom ( ~~>t ` J ) )
6 2 5 jca 
 |-  ( D e. ( CMet ` X ) -> ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~>t ` J ) ) )
7 ssel2 
 |-  ( ( ( Cau ` D ) C_ dom ( ~~>t ` J ) /\ f e. ( Cau ` D ) ) -> f e. dom ( ~~>t ` J ) )
8 7 a1d 
 |-  ( ( ( Cau ` D ) C_ dom ( ~~>t ` J ) /\ f e. ( Cau ` D ) ) -> ( f : NN --> X -> f e. dom ( ~~>t ` J ) ) )
9 8 ralrimiva 
 |-  ( ( Cau ` D ) C_ dom ( ~~>t ` J ) -> A. f e. ( Cau ` D ) ( f : NN --> X -> f e. dom ( ~~>t ` J ) ) )
10 9 adantl 
 |-  ( ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~>t ` J ) ) -> A. f e. ( Cau ` D ) ( f : NN --> X -> f e. dom ( ~~>t ` J ) ) )
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 1zzd 
 |-  ( ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~>t ` J ) ) -> 1 e. ZZ )
13 simpl 
 |-  ( ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~>t ` J ) ) -> D e. ( Met ` X ) )
14 11 1 12 13 iscmet3 
 |-  ( ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~>t ` J ) ) -> ( D e. ( CMet ` X ) <-> A. f e. ( Cau ` D ) ( f : NN --> X -> f e. dom ( ~~>t ` J ) ) ) )
15 10 14 mpbird 
 |-  ( ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~>t ` J ) ) -> D e. ( CMet ` X ) )
16 6 15 impbii 
 |-  ( D e. ( CMet ` X ) <-> ( D e. ( Met ` X ) /\ ( Cau ` D ) C_ dom ( ~~>t ` J ) ) )