Theorem iscmet3i

Description: Properties that determine a complete metric space. (Contributed by NM, 15-Apr-2007) (Revised by Mario Carneiro, 5-May-2014)

	Ref	Expression
Hypotheses	iscmet3i.2	|- J = ( MetOpen ` D )
	iscmet3i.3	|- D e. ( Met ` X )
	iscmet3i.4	|- ( ( f e. ( Cau ` D ) /\ f : NN --> X ) -> f e. dom ( ~~>t ` J ) )
Assertion	iscmet3i	|- D e. ( CMet ` X )

Proof

Step	Hyp	Ref	Expression
1		iscmet3i.2	|- J = ( MetOpen ` D )
2		iscmet3i.3	|- D e. ( Met ` X )
3		iscmet3i.4	|- ( ( f e. ( Cau ` D ) /\ f : NN --> X ) -> f e. dom ( ~~>t ` J ) )
4		nnuz	|- NN = ( ZZ>= ` 1 )
5		1zzd	|- ( T. -> 1 e. ZZ )
6	2	a1i	|- ( T. -> D e. ( Met ` X ) )
7	4 1 5 6	iscmet3	|- ( T. -> ( D e. ( CMet ` X ) <-> A. f e. ( Cau ` D ) ( f : NN --> X -> f e. dom ( ~~>t ` J ) ) ) )
8	7	mptru	|- ( D e. ( CMet ` X ) <-> A. f e. ( Cau ` D ) ( f : NN --> X -> f e. dom ( ~~>t ` J ) ) )
9	3	ex	|- ( f e. ( Cau ` D ) -> ( f : NN --> X -> f e. dom ( ~~>t ` J ) ) )
10	8 9	mprgbir	|- D e. ( CMet ` X )