Definition df-ee 26383

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

Assertion

Ref	Expression
df-ee	⊢ 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑𝑚 (1...𝑛)))

Detailed syntax breakdown of Definition df-ee

Step	Hyp	Ref	Expression
1		cee 26380	. 2 class 𝔼
2		vn	. . 3 setvar 𝑛
3		cn 11441	. . 3 class ℕ
4		cr 10336	. . . 4 class ℝ
5		c1 10338	. . . . 5 class 1
6	2	cv 1506	. . . . 5 class 𝑛
7		cfz 12711	. . . . 5 class ...
8	5, 6, 7	co 6978	. . . 4 class (1...𝑛)
9		cmap 8208	. . . 4 class ↑𝑚
10	4, 8, 9	co 6978	. . 3 class (ℝ ↑𝑚 (1...𝑛))
11	2, 3, 10	cmpt 5009	. 2 class (𝑛 ∈ ℕ ↦ (ℝ ↑𝑚 (1...𝑛)))
12	1, 11	wceq 1507	1 wff 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑𝑚 (1...𝑛)))

This definition is referenced by:  elee  26386  eleenn  26388  eenglngeehlnm  44095