| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-ee | Structured version Visualization version GIF version | ||
| Description: Define the Euclidean space generator. For details, see elee 28909. (Contributed by Scott Fenton, 3-Jun-2013.) |
| Ref | Expression |
|---|---|
| df-ee | ⊢ 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑m (1...𝑛))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cee 28903 | . 2 class 𝔼 | |
| 2 | vn | . . 3 setvar 𝑛 | |
| 3 | cn 12266 | . . 3 class ℕ | |
| 4 | cr 11154 | . . . 4 class ℝ | |
| 5 | c1 11156 | . . . . 5 class 1 | |
| 6 | 2 | cv 1539 | . . . . 5 class 𝑛 |
| 7 | cfz 13547 | . . . . 5 class ... | |
| 8 | 5, 6, 7 | co 7431 | . . . 4 class (1...𝑛) |
| 9 | cmap 8866 | . . . 4 class ↑m | |
| 10 | 4, 8, 9 | co 7431 | . . 3 class (ℝ ↑m (1...𝑛)) |
| 11 | 2, 3, 10 | cmpt 5225 | . 2 class (𝑛 ∈ ℕ ↦ (ℝ ↑m (1...𝑛))) |
| 12 | 1, 11 | wceq 1540 | 1 wff 𝔼 = (𝑛 ∈ ℕ ↦ (ℝ ↑m (1...𝑛))) |
| Colors of variables: wff setvar class |
| This definition is referenced by: elee 28909 eleenn 28911 eenglngeehlnm 48660 |
| Copyright terms: Public domain | W3C validator |