Theorem eleenn

Description: If A is in ( EEN ) , then N is a natural. (Contributed by Scott Fenton, 1-Jul-2013)

	Ref	Expression
Assertion	eleenn	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		df-ee	⊢ 𝔼 = ( 𝑛 ∈ ℕ ↦ ( ℝ ↑m ( 1 ... 𝑛 ) ) )
2	1	mptrcl	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )