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 e. NN -> ( A e. ( EE ` N ) <-> A : ( 1 ... N ) --> RR ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
2	1	oveq2d	|- ( n = N -> ( RR ^m ( 1 ... n ) ) = ( RR ^m ( 1 ... N ) ) )
3		df-ee	|- EE = ( n e. NN |-> ( RR ^m ( 1 ... n ) ) )
4		ovex	|- ( RR ^m ( 1 ... N ) ) e. _V
5	2 3 4	fvmpt	|- ( N e. NN -> ( EE ` N ) = ( RR ^m ( 1 ... N ) ) )
6	5	eleq2d	|- ( N e. NN -> ( A e. ( EE ` N ) <-> A e. ( RR ^m ( 1 ... N ) ) ) )
7		reex	|- RR e. _V
8		ovex	|- ( 1 ... N ) e. _V
9	7 8	elmap	|- ( A e. ( RR ^m ( 1 ... N ) ) <-> A : ( 1 ... N ) --> RR )
10	6 9	bitrdi	|- ( N e. NN -> ( A e. ( EE ` N ) <-> A : ( 1 ... N ) --> RR ) )