Description: Lemma for elovolm and related theorems. (Contributed by BJ, 23-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | elovolmlem | ⊢ ( 𝐹 ∈ ( ( 𝐴 ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( 𝐴 ∩ ( ℝ × ℝ ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reex | ⊢ ℝ ∈ V | |
2 | 1 1 | xpex | ⊢ ( ℝ × ℝ ) ∈ V |
3 | 2 | inex2 | ⊢ ( 𝐴 ∩ ( ℝ × ℝ ) ) ∈ V |
4 | nnex | ⊢ ℕ ∈ V | |
5 | 3 4 | elmap | ⊢ ( 𝐹 ∈ ( ( 𝐴 ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( 𝐴 ∩ ( ℝ × ℝ ) ) ) |