Theorem frexr 46611

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ⟶wf 6557  ℝcr 11229  ℝ^*cxr 11372

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-f 6565  df-xr 11377

This theorem is used by:  limsupubuz  46938  limsupreuz  46962  limsupvaluz2  46963  supcnvlimsup  46965  limsupgtlem  47002  liminflimsupclim  47032  climliminflimsup2  47034  climliminflimsup3  47035  climliminflimsup4  47036  xlimliminflimsup  47087  hoicvr  47773  preimaioomnf  47944  incsmf  47967  issmfle  47970  decsmf  47992  smfsupdmmbllem  48069  smfinfdmmbllem  48073