Theorem elovolmlem

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

	Ref	Expression
Assertion	elovolmlem	⊢ ( 𝐹 ∈ ( ( 𝐴 ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( 𝐴 ∩ ( ℝ × ℝ ) ) )

Proof

Step	Hyp	Ref	Expression
1		reex	⊢ ℝ ∈ V
2	1 1	xpex	⊢ ( ℝ × ℝ ) ∈ V
3	2	inex2	⊢ ( 𝐴 ∩ ( ℝ × ℝ ) ) ∈ V
4		nnex	⊢ ℕ ∈ V
5	3 4	elmap	⊢ ( 𝐹 ∈ ( ( 𝐴 ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( 𝐴 ∩ ( ℝ × ℝ ) ) )