This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elovolmlem

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

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

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