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	$$⊢𝔼=\left(n\in \mathbb{N}⟼{ℝ}^{\left(1\dots n\right)}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cee	$$class𝔼$$
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3		cr	$$classℝ$$
4		cmap	$$class{\uparrow }_{𝑚}$$
5		c1	$$class1$$
6		cfz	$$class\dots$$
7	1	cv	$$setvarn$$
8	5 7 6	co	$$class\left(1\dots n\right)$$
9	3 8 4	co	$$class\left({ℝ}^{\left(1\dots n\right)}\right)$$
10	1 2 9	cmpt	$$class\left(n\in \mathbb{N}⟼{ℝ}^{\left(1\dots n\right)}\right)$$
11	0 10	wceq	$$wff𝔼=\left(n\in \mathbb{N}⟼{ℝ}^{\left(1\dots n\right)}\right)$$