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

Metamath Proof Explorer

Theorem frexr

Description: A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis frexr.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
Assertion frexr ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )

Proof

Step Hyp Ref Expression
1 frexr.1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
2 ressxr ⊢ ℝ ⊆ ℝ*
3 2 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
4 1 3 fssd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )