Theorem eleei

Description: The forward direction of elee . (Contributed by Scott Fenton, 1-Jul-2013)

	Ref	Expression
Assertion	eleei	|- ( A e. ( EE ` N ) -> A : ( 1 ... N ) --> RR )

Proof

Step	Hyp	Ref	Expression
1		eleenn	|- ( A e. ( EE ` N ) -> N e. NN )
2		elee	|- ( N e. NN -> ( A e. ( EE ` N ) <-> A : ( 1 ... N ) --> RR ) )
3	1 2	syl	|- ( A e. ( EE ` N ) -> ( A e. ( EE ` N ) <-> A : ( 1 ... N ) --> RR ) )
4	3	ibi	|- ( A e. ( EE ` N ) -> A : ( 1 ... N ) --> RR )