Step |
Hyp |
Ref |
Expression |
1 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
2 |
|
fss |
|- ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR ) |
3 |
1 2
|
mpan2 |
|- ( F : RR --> ( 0 [,) +oo ) -> F : RR --> RR ) |
4 |
|
ffvelrn |
|- ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) e. RR ) |
5 |
|
elrege0 |
|- ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) ) |
6 |
5
|
baib |
|- ( ( F ` x ) e. RR -> ( ( F ` x ) e. ( 0 [,) +oo ) <-> 0 <_ ( F ` x ) ) ) |
7 |
4 6
|
syl |
|- ( ( F : RR --> RR /\ x e. RR ) -> ( ( F ` x ) e. ( 0 [,) +oo ) <-> 0 <_ ( F ` x ) ) ) |
8 |
7
|
ralbidva |
|- ( F : RR --> RR -> ( A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) <-> A. x e. RR 0 <_ ( F ` x ) ) ) |
9 |
|
ffn |
|- ( F : RR --> RR -> F Fn RR ) |
10 |
|
ffnfv |
|- ( F : RR --> ( 0 [,) +oo ) <-> ( F Fn RR /\ A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) ) ) |
11 |
10
|
baib |
|- ( F Fn RR -> ( F : RR --> ( 0 [,) +oo ) <-> A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) ) ) |
12 |
9 11
|
syl |
|- ( F : RR --> RR -> ( F : RR --> ( 0 [,) +oo ) <-> A. x e. RR ( F ` x ) e. ( 0 [,) +oo ) ) ) |
13 |
|
0cn |
|- 0 e. CC |
14 |
|
fnconstg |
|- ( 0 e. CC -> ( CC X. { 0 } ) Fn CC ) |
15 |
13 14
|
ax-mp |
|- ( CC X. { 0 } ) Fn CC |
16 |
|
df-0p |
|- 0p = ( CC X. { 0 } ) |
17 |
16
|
fneq1i |
|- ( 0p Fn CC <-> ( CC X. { 0 } ) Fn CC ) |
18 |
15 17
|
mpbir |
|- 0p Fn CC |
19 |
18
|
a1i |
|- ( F : RR --> RR -> 0p Fn CC ) |
20 |
|
cnex |
|- CC e. _V |
21 |
20
|
a1i |
|- ( F : RR --> RR -> CC e. _V ) |
22 |
|
reex |
|- RR e. _V |
23 |
22
|
a1i |
|- ( F : RR --> RR -> RR e. _V ) |
24 |
|
ax-resscn |
|- RR C_ CC |
25 |
|
sseqin2 |
|- ( RR C_ CC <-> ( CC i^i RR ) = RR ) |
26 |
24 25
|
mpbi |
|- ( CC i^i RR ) = RR |
27 |
|
0pval |
|- ( x e. CC -> ( 0p ` x ) = 0 ) |
28 |
27
|
adantl |
|- ( ( F : RR --> RR /\ x e. CC ) -> ( 0p ` x ) = 0 ) |
29 |
|
eqidd |
|- ( ( F : RR --> RR /\ x e. RR ) -> ( F ` x ) = ( F ` x ) ) |
30 |
19 9 21 23 26 28 29
|
ofrfval |
|- ( F : RR --> RR -> ( 0p oR <_ F <-> A. x e. RR 0 <_ ( F ` x ) ) ) |
31 |
8 12 30
|
3bitr4d |
|- ( F : RR --> RR -> ( F : RR --> ( 0 [,) +oo ) <-> 0p oR <_ F ) ) |
32 |
3 31
|
biadanii |
|- ( F : RR --> ( 0 [,) +oo ) <-> ( F : RR --> RR /\ 0p oR <_ F ) ) |