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	⊢ 𝔼 = ( 𝑛 ∈ ℕ ↦ ( ℝ ↑m ( 1 ... 𝑛 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cee	⊢ 𝔼
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3		cr	⊢ ℝ
4		cmap	⊢ ↑m
5		c1	⊢ 1
6		cfz	⊢ ...
7	1	cv	⊢ 𝑛
8	5 7 6	co	⊢ ( 1 ... 𝑛 )
9	3 8 4	co	⊢ ( ℝ ↑m ( 1 ... 𝑛 ) )
10	1 2 9	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( ℝ ↑m ( 1 ... 𝑛 ) ) )
11	0 10	wceq	⊢ 𝔼 = ( 𝑛 ∈ ℕ ↦ ( ℝ ↑m ( 1 ... 𝑛 ) ) )