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 44095
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 11258 . . 3 ℝ βŠ† ℝ*
32a1i 11 . 2 (πœ‘ β†’ ℝ βŠ† ℝ*)
41, 3fssd 6736 1 (πœ‘ β†’ 𝐹:π΄βŸΆβ„*)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   βŠ† wss 3949  βŸΆwf 6540  β„cr 11109  β„*cxr 11247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-f 6548  df-xr 11252
This theorem is referenced by:  limsupubuz  44429  limsupreuz  44453  limsupvaluz2  44454  supcnvlimsup  44456  limsupgtlem  44493  liminflimsupclim  44523  climliminflimsup2  44525  climliminflimsup3  44526  climliminflimsup4  44527  xlimliminflimsup  44578  preimaioomnf  45435  incsmf  45458  issmfle  45461  decsmf  45483  smfsupdmmbllem  45560  smfinfdmmbllem  45564
  Copyright terms: Public domain W3C validator