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 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
rrxf.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
Assertion rrxf ( 𝜑 → 𝐹 : 𝐼 ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 rrxmval.1 ⊢ 𝑋 = { ℎ ∈ ( ℝ ↑m 𝐼 ) ∣ ℎ finSupp 0 }
2 rrxf.1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
3 1 ssrab3 ⊢ 𝑋 ⊆ ( ℝ ↑m 𝐼 )
4 3 2 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ ↑m 𝐼 ) )
5 elmapi ⊢ ( 𝐹 ∈ ( ℝ ↑m 𝐼 ) → 𝐹 : 𝐼 ⟶ ℝ )
6 4 5 syl ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ℝ )