Metamath Proof Explorer

Definition df-ee

Description: Define the Euclidean space generator. For details, see elee . (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion df-ee 
|- EE = ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cee 
 |-  EE
1 vn 
 |-  n
2 cn 
 |-  NN
3 cr 
 |-  RR
4 cmap 
 |-  ^m
5 c1 
 |-  1
6 cfz 
 |-  ...
7 1 cv 
 |-  n
8 5 7 6 co 
 |-  ( 1 ... n )
9 3 8 4 co 
 |-  ( RR ^m ( 1 ... n ) )
10 1 2 9 cmpt 
 |-  ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )
11 0 10 wceq 
 |-  EE = ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )