Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frexr Structured version   Visualization version   GIF version

Theorem frexr 45334
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
StepHypRef Expression
1 frexr.1 . 2 (𝜑𝐹:𝐴⟶ℝ)
2 ressxr 11302 . . 3 ℝ ⊆ ℝ*
32a1i 11 . 2 (𝜑 → ℝ ⊆ ℝ*)
41, 3fssd 6753 1 (𝜑𝐹:𝐴⟶ℝ*)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3962  wf 6558  cr 11151  *cxr 11291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979  df-f 6566  df-xr 11296
This theorem is referenced by:  limsupubuz  45668  limsupreuz  45692  limsupvaluz2  45693  supcnvlimsup  45695  limsupgtlem  45732  liminflimsupclim  45762  climliminflimsup2  45764  climliminflimsup3  45765  climliminflimsup4  45766  xlimliminflimsup  45817  preimaioomnf  46674  incsmf  46697  issmfle  46700  decsmf  46722  smfsupdmmbllem  46799  smfinfdmmbllem  46803
  Copyright terms: Public domain W3C validator