Metamath Proof Explorer

Theorem fge0iccico

Description: A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fge0iccico.f 
|- ( ph -> F : X --> ( 0 [,] +oo ) )
fge0iccico.re 
|- ( ph -> -. +oo e. ran F )
Assertion fge0iccico 
|- ( ph -> F : X --> ( 0 [,) +oo ) )

Proof

Step Hyp Ref Expression
1 fge0iccico.f 
 |-  ( ph -> F : X --> ( 0 [,] +oo ) )
2 fge0iccico.re 
 |-  ( ph -> -. +oo e. ran F )
3 1 ffnd 
 |-  ( ph -> F Fn X )
4 0xr 
 |-  0 e. RR*
5 4 a1i 
 |-  ( ( ph /\ x e. X ) -> 0 e. RR* )
6 pnfxr 
 |-  +oo e. RR*
7 6 a1i 
 |-  ( ( ph /\ x e. X ) -> +oo e. RR* )
8 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
9 1 ffvelcdmda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. ( 0 [,] +oo ) )
10 8 9 sselid 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. RR* )
11 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( F ` x ) e. ( 0 [,] +oo ) ) -> 0 <_ ( F ` x ) )
12 5 7 9 11 syl3anc 
 |-  ( ( ph /\ x e. X ) -> 0 <_ ( F ` x ) )
13 10 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> ( F ` x ) e. RR* )
14 simpr 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> -. ( F ` x ) < +oo )
15 6 a1i 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> +oo e. RR* )
16 15 13 xrlenltd 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> ( +oo <_ ( F ` x ) <-> -. ( F ` x ) < +oo ) )
17 14 16 mpbird 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> +oo <_ ( F ` x ) )
18 13 17 xrgepnfd 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> ( F ` x ) = +oo )
19 18 eqcomd 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> +oo = ( F ` x ) )
20 1 ffund 
 |-  ( ph -> Fun F )
21 20 adantr 
 |-  ( ( ph /\ x e. X ) -> Fun F )
22 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
23 fdm 
 |-  ( F : X --> ( 0 [,] +oo ) -> dom F = X )
24 23 eqcomd 
 |-  ( F : X --> ( 0 [,] +oo ) -> X = dom F )
25 1 24 syl 
 |-  ( ph -> X = dom F )
26 25 adantr 
 |-  ( ( ph /\ x e. X ) -> X = dom F )
27 22 26 eleqtrd 
 |-  ( ( ph /\ x e. X ) -> x e. dom F )
28 fvelrn 
 |-  ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F )
29 21 27 28 syl2anc 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. ran F )
30 29 adantr 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> ( F ` x ) e. ran F )
31 19 30 eqeltrd 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> +oo e. ran F )
32 2 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ -. ( F ` x ) < +oo ) -> -. +oo e. ran F )
33 31 32 condan 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) < +oo )
34 5 7 10 12 33 elicod 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. ( 0 [,) +oo ) )
35 34 ralrimiva 
 |-  ( ph -> A. x e. X ( F ` x ) e. ( 0 [,) +oo ) )
36 3 35 jca 
 |-  ( ph -> ( F Fn X /\ A. x e. X ( F ` x ) e. ( 0 [,) +oo ) ) )
37 ffnfv 
 |-  ( F : X --> ( 0 [,) +oo ) <-> ( F Fn X /\ A. x e. X ( F ` x ) e. ( 0 [,) +oo ) ) )
38 36 37 sylibr 
 |-  ( ph -> F : X --> ( 0 [,) +oo ) )