Theorem frexr 45360

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

Syntax hints:   → wi 4   ⊆ wss 3926  ⟶wf 6526  ℝcr 11126  ℝ^*cxr 11266

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-f 6534  df-xr 11271

This theorem is referenced by:  limsupubuz  45690  limsupreuz  45714  limsupvaluz2  45715  supcnvlimsup  45717  limsupgtlem  45754  liminflimsupclim  45784  climliminflimsup2  45786  climliminflimsup3  45787  climliminflimsup4  45788  xlimliminflimsup  45839  preimaioomnf  46696  incsmf  46719  issmfle  46722  decsmf  46744  smfsupdmmbllem  46821  smfinfdmmbllem  46825