Metamath Proof Explorer

Theorem xrge0f

Description: A real function is a nonnegative extended real function if all its values are greater than or equal to zero. (Contributed by Mario Carneiro, 28-Jun-2014) (Revised by Mario Carneiro, 28-Jul-2014)

Ref Expression
Assertion xrge0f 
|- ( ( F : RR --> RR /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : RR --> RR -> F Fn RR )
2 1 adantr 
 |-  ( ( F : RR --> RR /\ 0p oR <_ F ) -> F Fn RR )
3 ax-resscn 
 |-  RR C_ CC
4 3 a1i 
 |-  ( F : RR --> RR -> RR C_ CC )
5 4 1 0pledm 
 |-  ( F : RR --> RR -> ( 0p oR <_ F <-> ( RR X. { 0 } ) oR <_ F ) )
6 0re 
 |-  0 e. RR
7 fnconstg 
 |-  ( 0 e. RR -> ( RR X. { 0 } ) Fn RR )
8 6 7 mp1i 
 |-  ( F : RR --> RR -> ( RR X. { 0 } ) Fn RR )
9 reex 
 |-  RR e. _V
10 9 a1i 
 |-  ( F : RR --> RR -> RR e. _V )
11 inidm 
 |-  ( RR i^i RR ) = RR
12 c0ex 
 |-  0 e. _V
13 12 fvconst2 
 |-  ( x e. RR -> ( ( RR X. { 0 } ) ` x ) = 0 )
14 13 adantl 
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( ( RR X. { 0 } ) ` x ) = 0 )
15 eqidd 
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) = ( F ` x ) )
16 8 1 10 10 11 14 15 ofrfval 
 |-  ( F : RR --> RR -> ( ( RR X. { 0 } ) oR <_ F <-> A. x e. RR 0 <_ ( F ` x ) ) )
17 ffvelrn 
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) e. RR )
18 17 rexrd 
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) e. RR* )
19 18 biantrurd 
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) ) )
20 elxrge0 
 |-  ( ( F ` x ) e. ( 0 [,] +oo ) <-> ( ( F ` x ) e. RR* /\ 0 <_ ( F ` x ) ) )
21 19 20 bitr4di 
 |-  ( ( F : RR --> RR /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> ( F ` x ) e. ( 0 [,] +oo ) ) )
22 21 ralbidva 
 |-  ( F : RR --> RR -> ( A. x e. RR 0 <_ ( F ` x ) <-> A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) ) )
23 5 16 22 3bitrd 
 |-  ( F : RR --> RR -> ( 0p oR <_ F <-> A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) ) )
24 23 biimpa 
 |-  ( ( F : RR --> RR /\ 0p oR <_ F ) -> A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) )
25 ffnfv 
 |-  ( F : RR --> ( 0 [,] +oo ) <-> ( F Fn RR /\ A. x e. RR ( F ` x ) e. ( 0 [,] +oo ) ) )
26 2 24 25 sylanbrc 
 |-  ( ( F : RR --> RR /\ 0p oR <_ F ) -> F : RR --> ( 0 [,] +oo ) )