MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ee Structured version   Visualization version   GIF version

Definition df-ee 25485
Description: Define the Euclidean space generator. For details, see elee 25488. (Contributed by Scott Fenton, 3-Jun-2013.)
Assertion
Ref Expression
df-ee 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑𝑚 (1...𝑛)))

Detailed syntax breakdown of Definition df-ee
StepHypRef Expression
1 cee 25482 . 2 class 𝔼
2 vn . . 3 setvar 𝑛
3 cn 10863 . . 3 class
4 cr 9787 . . . 4 class
5 c1 9789 . . . . 5 class 1
62cv 1473 . . . . 5 class 𝑛
7 cfz 12148 . . . . 5 class ...
85, 6, 7co 6523 . . . 4 class (1...𝑛)
9 cmap 7717 . . . 4 class 𝑚
104, 8, 9co 6523 . . 3 class (ℝ ↑𝑚 (1...𝑛))
112, 3, 10cmpt 4633 . 2 class (𝑛 ∈ ℕ ↦ (ℝ ↑𝑚 (1...𝑛)))
121, 11wceq 1474 1 wff 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑𝑚 (1...𝑛)))
Colors of variables: wff setvar class
This definition is referenced by:  elee  25488  eleenn  25490
  Copyright terms: Public domain W3C validator