Theorem eleenn

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

	Ref	Expression
Assertion	eleenn	$$⊢A\in 𝔼\left(N\right)\to N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		df-ee	$$⊢𝔼=\left(n\in \mathbb{N}⟼{ℝ}^{\left(1\dots n\right)}\right)$$
2	1	mptrcl	$$⊢A\in 𝔼\left(N\right)\to N\in \mathbb{N}$$