Definition df-ee 25771

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

Assertion

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

Detailed syntax breakdown of Definition df-ee

Step	Hyp	Ref	Expression
1		cee 25768	. 2 class EE
2		vn	. . 3 setvar n
3		cn 11020	. . 3 class NN
4		cr 9935	. . . 4 class RR
5		c1 9937	. . . . 5 class 1
6	2	cv 1482	. . . . 5 class n
7		cfz 12326	. . . . 5 class ...
8	5, 6, 7	co 6650	. . . 4 class ( 1 ... n )
9		cmap 7857	. . . 4 class ^m
10	4, 8, 9	co 6650	. . 3 class ( RR ^m ( 1 ... n ) )
11	2, 3, 10	cmpt 4729	. 2 class ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )
12	1, 11	wceq 1483	1 wff EE = ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )

This definition is referenced by:  elee  25774  eleenn  25776