Theorem frexr 45300

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

Syntax hints:   → wi 4   ⊆ wss 3976  ⟶wf 6569  ℝcr 11183  ℝ^*cxr 11323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-f 6577  df-xr 11328

This theorem is referenced by:  limsupubuz  45634  limsupreuz  45658  limsupvaluz2  45659  supcnvlimsup  45661  limsupgtlem  45698  liminflimsupclim  45728  climliminflimsup2  45730  climliminflimsup3  45731  climliminflimsup4  45732  xlimliminflimsup  45783  preimaioomnf  46640  incsmf  46663  issmfle  46666  decsmf  46688  smfsupdmmbllem  46765  smfinfdmmbllem  46769