Theorem frexr 46222

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902  ⟶wf 6533  ℝcr 11127  ℝ^*cxr 11270

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-f 6541  df-xr 11275

This theorem is used by:  limsupubuz  46549  limsupreuz  46573  limsupvaluz2  46574  supcnvlimsup  46576  limsupgtlem  46613  liminflimsupclim  46643  climliminflimsup2  46645  climliminflimsup3  46646  climliminflimsup4  46647  xlimliminflimsup  46698  hoicvr  47384  preimaioomnf  47555  incsmf  47578  issmfle  47581  decsmf  47603  smfsupdmmbllem  47680  smfinfdmmbllem  47684