Theorem rrxf

Description: Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019)

	Ref	Expression
Hypotheses	rrxmval.1	$$⊢X=\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}$$
	rrxf.1	$$⊢\phi \to F\in X$$
Assertion	rrxf	$$⊢\phi \to F:I⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		rrxmval.1	$$⊢X=\left\{h\in \left({ℝ}^I\right)|{finSupp}_0\left(h\right)\right\}$$
2		rrxf.1	$$⊢\phi \to F\in X$$
3	1	ssrab3	$$⊢X\subseteq {ℝ}^I$$
4	3 2	sselid	$$⊢\phi \to F\in \left({ℝ}^I\right)$$
5		elmapi	$$⊢F\in \left({ℝ}^I\right)\to F:I⟶ℝ$$
6	4 5	syl	$$⊢\phi \to F:I⟶ℝ$$