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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ* )