![]() |
Mathbox for Glauco Siliprandi |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > frexr | Structured version Visualization version GIF version |
Description: A function taking real values, is a function taking extended real values. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
frexr.1 | ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) |
Ref | Expression |
---|---|
frexr | ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frexr.1 | . 2 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ) | |
2 | ressxr 11302 | . . 3 ⊢ ℝ ⊆ ℝ* | |
3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → ℝ ⊆ ℝ*) |
4 | 1, 3 | fssd 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 |