Description: The forward direction of elee . (Contributed by Scott Fenton, 1-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | eleei | ⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleenn | ⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ ) | |
2 | elee | ⊢ ( 𝑁 ∈ ℕ → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) | |
3 | 1 2 | syl | ⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) ) |
4 | 3 | ibi | ⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ) |