Theorem frexr 45365

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 11178	. . 3 ⊢ ℝ ⊆ ℝ*
3	2	a1i 11	. 2 ⊢ (𝜑 → ℝ ⊆ ℝ*)
4	1, 3	fssd 6673	1 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)

Syntax hints:   → wi 4   ⊆ wss 3905  ⟶wf 6482  ℝcr 11027  ℝ^*cxr 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-f 6490  df-xr 11172

This theorem is referenced by:  limsupubuz  45695  limsupreuz  45719  limsupvaluz2  45720  supcnvlimsup  45722  limsupgtlem  45759  liminflimsupclim  45789  climliminflimsup2  45791  climliminflimsup3  45792  climliminflimsup4  45793  xlimliminflimsup  45844  preimaioomnf  46701  incsmf  46724  issmfle  46727  decsmf  46749  smfsupdmmbllem  46826  smfinfdmmbllem  46830