Theorem eleei

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

	Ref	Expression
Assertion	eleei	$$⊢A\in 𝔼\left(N\right)\to A:\left(1\dots N\right)⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eleenn	$$⊢A\in 𝔼\left(N\right)\to N\in \mathbb{N}$$
2		elee	$$⊢N\in \mathbb{N}\to \left(A\in 𝔼\left(N\right)\leftrightarrow A:\left(1\dots N\right)⟶ℝ\right)$$
3	1 2	syl	$$⊢A\in 𝔼\left(N\right)\to \left(A\in 𝔼\left(N\right)\leftrightarrow A:\left(1\dots N\right)⟶ℝ\right)$$
4	3	ibi	$$⊢A\in 𝔼\left(N\right)\to A:\left(1\dots N\right)⟶ℝ$$