Metamath Proof Explorer


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 ℕ ) ↔ 𝐹 : ℕ ⟶ ( 𝐴 ∩ ( ℝ × ℝ ) ) )