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

Metamath Proof Explorer

Theorem rrxf

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

Ref Expression
Hypotheses rrxmval.1 ⊢ X = h ∈ ℝ I | finSupp 0 ⁡ h
rrxf.1 ⊢ φ → F ∈ X
Assertion rrxf ⊢ φ → F : I ⟶ ℝ

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ X = h ∈ ℝ I | finSupp 0 ⁡ h
2 rrxf.1 ⊢ φ → F ∈ X
3 1 ssrab3 ⊢ X ⊆ ℝ I
4 3 2 sselid ⊢ φ → F ∈ ℝ I
5 elmapi ⊢ F ∈ ℝ I → F : I ⟶ ℝ
6 4 5 syl ⊢ φ → F : I ⟶ ℝ