Metamath Proof Explorer

Theorem rrncms

Description: Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis rrncms.1 
|- X = ( RR ^m I )
Assertion rrncms 
|- ( I e. Fin -> ( Rn ` I ) e. ( CMet ` X ) )

Proof

Step Hyp Ref Expression
1 rrncms.1 
 |-  X = ( RR ^m I )
2 eqid 
 |-  ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
3 eqid 
 |-  ( MetOpen ` ( Rn ` I ) ) = ( MetOpen ` ( Rn ` I ) )
4 simpll 
 |-  ( ( ( I e. Fin /\ f e. ( Cau ` ( Rn ` I ) ) ) /\ f : NN --> X ) -> I e. Fin )
5 simplr 
 |-  ( ( ( I e. Fin /\ f e. ( Cau ` ( Rn ` I ) ) ) /\ f : NN --> X ) -> f e. ( Cau ` ( Rn ` I ) ) )
6 simpr 
 |-  ( ( ( I e. Fin /\ f e. ( Cau ` ( Rn ` I ) ) ) /\ f : NN --> X ) -> f : NN --> X )
7 eqid 
 |-  ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( f ` t ) ` m ) ) ) ) = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( f ` t ) ` m ) ) ) )
8 1 2 3 4 5 6 7 rrncmslem 
 |-  ( ( ( I e. Fin /\ f e. ( Cau ` ( Rn ` I ) ) ) /\ f : NN --> X ) -> f e. dom ( ~~>t ` ( MetOpen ` ( Rn ` I ) ) ) )
9 8 ex 
 |-  ( ( I e. Fin /\ f e. ( Cau ` ( Rn ` I ) ) ) -> ( f : NN --> X -> f e. dom ( ~~>t ` ( MetOpen ` ( Rn ` I ) ) ) ) )
10 9 ralrimiva 
 |-  ( I e. Fin -> A. f e. ( Cau ` ( Rn ` I ) ) ( f : NN --> X -> f e. dom ( ~~>t ` ( MetOpen ` ( Rn ` I ) ) ) ) )
11 nnuz 
 |-  NN = ( ZZ>= ` 1 )
12 1zzd 
 |-  ( I e. Fin -> 1 e. ZZ )
13 1 rrnmet 
 |-  ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
14 11 3 12 13 iscmet3 
 |-  ( I e. Fin -> ( ( Rn ` I ) e. ( CMet ` X ) <-> A. f e. ( Cau ` ( Rn ` I ) ) ( f : NN --> X -> f e. dom ( ~~>t ` ( MetOpen ` ( Rn ` I ) ) ) ) ) )
15 10 14 mpbird 
 |-  ( I e. Fin -> ( Rn ` I ) e. ( CMet ` X ) )