Metamath Proof Explorer

Theorem cncfioobd

Description: A continuous function F on an open interval ( A (,) B ) with a finite right limit R in A and a finite left limit L in B is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncfioobd.a 
|- ( ph -> A e. RR )
cncfioobd.b 
|- ( ph -> B e. RR )
cncfioobd.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
cncfioobd.l 
|- ( ph -> L e. ( F limCC B ) )
cncfioobd.r 
|- ( ph -> R e. ( F limCC A ) )
Assertion cncfioobd 
|- ( ph -> E. x e. RR A. y e. ( A (,) B ) ( abs ` ( F ` y ) ) <_ x )

Proof

Step Hyp Ref Expression
1 cncfioobd.a 
 |-  ( ph -> A e. RR )
2 cncfioobd.b 
 |-  ( ph -> B e. RR )
3 cncfioobd.f 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
4 cncfioobd.l 
 |-  ( ph -> L e. ( F limCC B ) )
5 cncfioobd.r 
 |-  ( ph -> R e. ( F limCC A ) )
6 nfv 
 |-  F/ z ph
7 eqid 
 |-  ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) = ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) )
8 6 7 1 2 3 4 5 cncfiooicc 
 |-  ( ph -> ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
9 cniccbdd 
 |-  ( ( A e. RR /\ B e. RR /\ ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x )
10 1 2 8 9 syl3anc 
 |-  ( ph -> E. x e. RR A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x )
11 nfv 
 |-  F/ y ( ph /\ x e. RR )
12 nfra1 
 |-  F/ y A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x
13 11 12 nfan 
 |-  F/ y ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x )
14 simpr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
15 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> CC ) -> F : ( A (,) B ) --> CC )
16 3 15 syl 
 |-  ( ph -> F : ( A (,) B ) --> CC )
17 16 fdmd 
 |-  ( ph -> dom F = ( A (,) B ) )
18 17 eqcomd 
 |-  ( ph -> ( A (,) B ) = dom F )
19 18 adantr 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( A (,) B ) = dom F )
20 14 19 eleqtrd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> y e. dom F )
21 1 adantr 
 |-  ( ( ph /\ y e. dom F ) -> A e. RR )
22 2 adantr 
 |-  ( ( ph /\ y e. dom F ) -> B e. RR )
23 16 adantr 
 |-  ( ( ph /\ y e. dom F ) -> F : ( A (,) B ) --> CC )
24 simpr 
 |-  ( ( ph /\ y e. dom F ) -> y e. dom F )
25 17 adantr 
 |-  ( ( ph /\ y e. dom F ) -> dom F = ( A (,) B ) )
26 24 25 eleqtrd 
 |-  ( ( ph /\ y e. dom F ) -> y e. ( A (,) B ) )
27 21 22 23 7 26 cncfioobdlem 
 |-  ( ( ph /\ y e. dom F ) -> ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) = ( F ` y ) )
28 20 27 syldan 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) = ( F ` y ) )
29 28 eqcomd 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( F ` y ) = ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) )
30 29 fveq2d 
 |-  ( ( ph /\ y e. ( A (,) B ) ) -> ( abs ` ( F ` y ) ) = ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) )
31 30 ad4ant14 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) /\ y e. ( A (,) B ) ) -> ( abs ` ( F ` y ) ) = ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) )
32 simplr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) /\ y e. ( A (,) B ) ) -> A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x )
33 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
34 simpr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) /\ y e. ( A (,) B ) ) -> y e. ( A (,) B ) )
35 33 34 sseldi 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) /\ y e. ( A (,) B ) ) -> y e. ( A [,] B ) )
36 rspa 
 |-  ( ( A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x /\ y e. ( A [,] B ) ) -> ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x )
37 32 35 36 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) /\ y e. ( A (,) B ) ) -> ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x )
38 31 37 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) /\ y e. ( A (,) B ) ) -> ( abs ` ( F ` y ) ) <_ x )
39 38 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) -> ( y e. ( A (,) B ) -> ( abs ` ( F ` y ) ) <_ x ) )
40 13 39 ralrimi 
 |-  ( ( ( ph /\ x e. RR ) /\ A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x ) -> A. y e. ( A (,) B ) ( abs ` ( F ` y ) ) <_ x )
41 40 ex 
 |-  ( ( ph /\ x e. RR ) -> ( A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x -> A. y e. ( A (,) B ) ( abs ` ( F ` y ) ) <_ x ) )
42 41 reximdva 
 |-  ( ph -> ( E. x e. RR A. y e. ( A [,] B ) ( abs ` ( ( z e. ( A [,] B ) |-> if ( z = A , R , if ( z = B , L , ( F ` z ) ) ) ) ` y ) ) <_ x -> E. x e. RR A. y e. ( A (,) B ) ( abs ` ( F ` y ) ) <_ x ) )
43 10 42 mpd 
 |-  ( ph -> E. x e. RR A. y e. ( A (,) B ) ( abs ` ( F ` y ) ) <_ x )