Theorem eleei

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

	Ref	Expression
Assertion	eleei	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eleenn	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
2		elee	⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) )
4	3	ibi	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ )