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

Metamath Proof Explorer

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 )