Theorem elovolmlem

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

	Ref	Expression
Assertion	elovolmlem	|- ( F e. ( ( A i^i ( RR X. RR ) ) ^m NN ) <-> F : NN --> ( A i^i ( RR X. RR ) ) )

Proof

Step	Hyp	Ref	Expression
1		reex	|- RR e. _V
2	1 1	xpex	|- ( RR X. RR ) e. _V
3	2	inex2	|- ( A i^i ( RR X. RR ) ) e. _V
4		nnex	|- NN e. _V
5	3 4	elmap	|- ( F e. ( ( A i^i ( RR X. RR ) ) ^m NN ) <-> F : NN --> ( A i^i ( RR X. RR ) ) )