Theorem elee

Description: Membership in a Euclidean space. We define Euclidean space here using Cartesian coordinates over N space. We later abstract away from this using Tarski's geometry axioms, so this exact definition is unimportant. (Contributed by Scott Fenton, 3-Jun-2013)

	Ref	Expression
Assertion	elee	$$⊢N\in \mathbb{N}\to \left(A\in 𝔼\left(N\right)\leftrightarrow A:\left(1\dots N\right)⟶ℝ\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢n=N\to \left(1\dots n\right)=\left(1\dots N\right)$$
2	1	oveq2d	$$⊢n=N\to {ℝ}^{\left(1\dots n\right)}={ℝ}^{\left(1\dots N\right)}$$
3		df-ee	$$⊢𝔼=\left(n\in \mathbb{N}⟼{ℝ}^{\left(1\dots n\right)}\right)$$
4		ovex	$$⊢{ℝ}^{\left(1\dots N\right)}\in \mathrm{V}$$
5	2 3 4	fvmpt	$$⊢N\in \mathbb{N}\to 𝔼\left(N\right)={ℝ}^{\left(1\dots N\right)}$$
6	5	eleq2d	$$⊢N\in \mathbb{N}\to \left(A\in 𝔼\left(N\right)\leftrightarrow A\in \left({ℝ}^{\left(1\dots N\right)}\right)\right)$$
7		reex	$$⊢ℝ\in \mathrm{V}$$
8		ovex	$$⊢\left(1\dots N\right)\in \mathrm{V}$$
9	7 8	elmap	$$⊢A\in \left({ℝ}^{\left(1\dots N\right)}\right)\leftrightarrow A:\left(1\dots N\right)⟶ℝ$$
10	6 9	bitrdi	$$⊢N\in \mathbb{N}\to \left(A\in 𝔼\left(N\right)\leftrightarrow A:\left(1\dots N\right)⟶ℝ\right)$$