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 ) ) )