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	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
2	1	oveq2d	⊢ ( 𝑛 = 𝑁 → ( ℝ ↑m ( 1 ... 𝑛 ) ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) )
3		df-ee	⊢ 𝔼 = ( 𝑛 ∈ ℕ ↦ ( ℝ ↑m ( 1 ... 𝑛 ) ) )
4		ovex	⊢ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∈ V
5	2 3 4	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( ℝ ↑m ( 1 ... 𝑁 ) ) )
6	5	eleq2d	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) )
7		reex	⊢ ℝ ∈ V
8		ovex	⊢ ( 1 ... 𝑁 ) ∈ V
9	7 8	elmap	⊢ ( 𝐴 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ )
10	6 9	bitrdi	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) )