Theorem frexr 44081

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

Syntax hints:   → wi 4   ⊆ wss 3947  ⟶wf 6536  ℝcr 11105  ℝ^*cxr 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-in 3954  df-ss 3964  df-f 6544  df-xr 11248

This theorem is referenced by:  limsupubuz  44415  limsupreuz  44439  limsupvaluz2  44440  supcnvlimsup  44442  limsupgtlem  44479  liminflimsupclim  44509  climliminflimsup2  44511  climliminflimsup3  44512  climliminflimsup4  44513  xlimliminflimsup  44564  preimaioomnf  45421  incsmf  45444  issmfle  45447  decsmf  45469  smfsupdmmbllem  45546  smfinfdmmbllem  45550