Theorem frexr 46141

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

Hypothesis

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

Assertion

Ref	Expression
frexr	⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)

Proof of Theorem frexr

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3908  ⟶wf 6539  ℝcr 11117  ℝ^*cxr 11260

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-f 6547  df-xr 11265

This theorem is used by:  limsupubuz  46468  limsupreuz  46492  limsupvaluz2  46493  supcnvlimsup  46495  limsupgtlem  46532  liminflimsupclim  46562  climliminflimsup2  46564  climliminflimsup3  46565  climliminflimsup4  46566  xlimliminflimsup  46617  hoicvr  47303  preimaioomnf  47474  incsmf  47497  issmfle  47500  decsmf  47522  smfsupdmmbllem  47599  smfinfdmmbllem  47603