Theorem elovolmlem

Description: Lemma for elovolm and related theorems. (Contributed by BJ, 23-Jul-2022)

	Ref	Expression
Assertion	elovolmlem	$$⊢F\in \left({\left(A\cap {ℝ}^2\right)}^{\mathbb{N}}\right)\leftrightarrow F:\mathbb{N}⟶A\cap {ℝ}^2$$

Proof

Step	Hyp	Ref	Expression
1		reex	$$⊢ℝ\in \mathrm{V}$$
2	1 1	xpex	$$⊢{ℝ}^2\in \mathrm{V}$$
3	2	inex2	$$⊢A\cap {ℝ}^2\in \mathrm{V}$$
4		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
5	3 4	elmap	$$⊢F\in \left({\left(A\cap {ℝ}^2\right)}^{\mathbb{N}}\right)\leftrightarrow F:\mathbb{N}⟶A\cap {ℝ}^2$$