Metamath Proof Explorer

Theorem extoimad

Description: If |f(x)| <= C for all x then it applies to all x in the image of |f(x)| (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses extoimad.1 
|- ( ph -> F : RR --> RR )
extoimad.2 
|- ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ C )
Assertion extoimad 
|- ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ C )

Proof

Step Hyp Ref Expression
1 extoimad.1 
 |-  ( ph -> F : RR --> RR )
2 extoimad.2 
 |-  ( ph -> A. y e. RR ( abs ` ( F ` y ) ) <_ C )
3 1 ffvelcdmda 
 |-  ( ( ph /\ y e. RR ) -> ( F ` y ) e. RR )
4 3 recnd 
 |-  ( ( ph /\ y e. RR ) -> ( F ` y ) e. CC )
5 4 abscld 
 |-  ( ( ph /\ y e. RR ) -> ( abs ` ( F ` y ) ) e. RR )
6 imaco 
 |-  ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) )
7 6 a1i 
 |-  ( ph -> ( ( abs o. F ) " RR ) = ( abs " ( F " RR ) ) )
8 7 eleq2d 
 |-  ( ph -> ( x e. ( ( abs o. F ) " RR ) <-> x e. ( abs " ( F " RR ) ) ) )
9 absf 
 |-  abs : CC --> RR
10 9 a1i 
 |-  ( ph -> abs : CC --> RR )
11 ax-resscn 
 |-  RR C_ CC
12 11 a1i 
 |-  ( ph -> RR C_ CC )
13 10 12 fssresd 
 |-  ( ph -> ( abs |` RR ) : RR --> RR )
14 1 13 fco2d 
 |-  ( ph -> ( abs o. F ) : RR --> RR )
15 14 ffnd 
 |-  ( ph -> ( abs o. F ) Fn RR )
16 ssidd 
 |-  ( ph -> RR C_ RR )
17 15 16 fvelimabd 
 |-  ( ph -> ( x e. ( ( abs o. F ) " RR ) <-> E. y e. RR ( ( abs o. F ) ` y ) = x ) )
18 eqcom 
 |-  ( ( ( abs o. F ) ` y ) = x <-> x = ( ( abs o. F ) ` y ) )
19 18 a1i 
 |-  ( ph -> ( ( ( abs o. F ) ` y ) = x <-> x = ( ( abs o. F ) ` y ) ) )
20 19 rexbidv 
 |-  ( ph -> ( E. y e. RR ( ( abs o. F ) ` y ) = x <-> E. y e. RR x = ( ( abs o. F ) ` y ) ) )
21 17 20 bitrd 
 |-  ( ph -> ( x e. ( ( abs o. F ) " RR ) <-> E. y e. RR x = ( ( abs o. F ) ` y ) ) )
22 1 adantr 
 |-  ( ( ph /\ y e. RR ) -> F : RR --> RR )
23 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
24 22 23 fvco3d 
 |-  ( ( ph /\ y e. RR ) -> ( ( abs o. F ) ` y ) = ( abs ` ( F ` y ) ) )
25 24 eqcomd 
 |-  ( ( ph /\ y e. RR ) -> ( abs ` ( F ` y ) ) = ( ( abs o. F ) ` y ) )
26 25 eqeq2d 
 |-  ( ( ph /\ y e. RR ) -> ( x = ( abs ` ( F ` y ) ) <-> x = ( ( abs o. F ) ` y ) ) )
27 26 rexbidva 
 |-  ( ph -> ( E. y e. RR x = ( abs ` ( F ` y ) ) <-> E. y e. RR x = ( ( abs o. F ) ` y ) ) )
28 21 27 bitr4d 
 |-  ( ph -> ( x e. ( ( abs o. F ) " RR ) <-> E. y e. RR x = ( abs ` ( F ` y ) ) ) )
29 8 28 bitr3d 
 |-  ( ph -> ( x e. ( abs " ( F " RR ) ) <-> E. y e. RR x = ( abs ` ( F ` y ) ) ) )
30 simpr 
 |-  ( ( ph /\ x = ( abs ` ( F ` y ) ) ) -> x = ( abs ` ( F ` y ) ) )
31 30 breq1d 
 |-  ( ( ph /\ x = ( abs ` ( F ` y ) ) ) -> ( x <_ C <-> ( abs ` ( F ` y ) ) <_ C ) )
32 5 29 31 ralxfr2d 
 |-  ( ph -> ( A. x e. ( abs " ( F " RR ) ) x <_ C <-> A. y e. RR ( abs ` ( F ` y ) ) <_ C ) )
33 2 32 mpbird 
 |-  ( ph -> A. x e. ( abs " ( F " RR ) ) x <_ C )