Metamath Proof Explorer

Theorem elbigo2

Description: Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020)

Ref Expression
Assertion elbigo2 
|- ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( F e. ( _O ` G ) <-> E. x e. RR E. m e. RR A. y e. B ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elbigo 
 |-  ( F e. ( _O ` G ) <-> ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
2 df-3an 
 |-  ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) <-> ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
3 1 2 bitri 
 |-  ( F e. ( _O ` G ) <-> ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
4 reex 
 |-  RR e. _V
5 4 4 pm3.2i 
 |-  ( RR e. _V /\ RR e. _V )
6 5 a1i 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( RR e. _V /\ RR e. _V ) )
7 simpl 
 |-  ( ( F : B --> RR /\ B C_ A ) -> F : B --> RR )
8 7 adantl 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> F : B --> RR )
9 sstr2 
 |-  ( B C_ A -> ( A C_ RR -> B C_ RR ) )
10 9 adantld 
 |-  ( B C_ A -> ( ( G : A --> RR /\ A C_ RR ) -> B C_ RR ) )
11 10 adantl 
 |-  ( ( F : B --> RR /\ B C_ A ) -> ( ( G : A --> RR /\ A C_ RR ) -> B C_ RR ) )
12 11 impcom 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> B C_ RR )
13 elpm2r 
 |-  ( ( ( RR e. _V /\ RR e. _V ) /\ ( F : B --> RR /\ B C_ RR ) ) -> F e. ( RR ^pm RR ) )
14 6 8 12 13 syl12anc 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> F e. ( RR ^pm RR ) )
15 simpl 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( G : A --> RR /\ A C_ RR ) )
16 elpm2r 
 |-  ( ( ( RR e. _V /\ RR e. _V ) /\ ( G : A --> RR /\ A C_ RR ) ) -> G e. ( RR ^pm RR ) )
17 6 15 16 syl2anc 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> G e. ( RR ^pm RR ) )
18 ibar 
 |-  ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) ) -> ( E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) <-> ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
19 18 bicomd 
 |-  ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) ) -> ( ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
20 14 17 19 syl2anc 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( ( ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
21 3 20 bitrid 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( F e. ( _O ` G ) <-> E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
22 elin 
 |-  ( y e. ( dom F i^i ( x [,) +oo ) ) <-> ( y e. dom F /\ y e. ( x [,) +oo ) ) )
23 fdm 
 |-  ( F : B --> RR -> dom F = B )
24 23 ad2antrl 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> dom F = B )
25 24 ad2antrr 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> dom F = B )
26 25 eleq2d 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( y e. dom F <-> y e. B ) )
27 26 anbi1d 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. dom F /\ y e. ( x [,) +oo ) ) <-> ( y e. B /\ y e. ( x [,) +oo ) ) ) )
28 elicopnf 
 |-  ( x e. RR -> ( y e. ( x [,) +oo ) <-> ( y e. RR /\ x <_ y ) ) )
29 28 ad3antlr 
 |-  ( ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) /\ y e. B ) -> ( y e. ( x [,) +oo ) <-> ( y e. RR /\ x <_ y ) ) )
30 12 ad2antrr 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> B C_ RR )
31 30 sselda 
 |-  ( ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) /\ y e. B ) -> y e. RR )
32 31 biantrurd 
 |-  ( ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) /\ y e. B ) -> ( x <_ y <-> ( y e. RR /\ x <_ y ) ) )
33 29 32 bitr4d 
 |-  ( ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) /\ y e. B ) -> ( y e. ( x [,) +oo ) <-> x <_ y ) )
34 33 pm5.32da 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. B /\ y e. ( x [,) +oo ) ) <-> ( y e. B /\ x <_ y ) ) )
35 27 34 bitrd 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. dom F /\ y e. ( x [,) +oo ) ) <-> ( y e. B /\ x <_ y ) ) )
36 22 35 bitrid 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( y e. ( dom F i^i ( x [,) +oo ) ) <-> ( y e. B /\ x <_ y ) ) )
37 36 imbi1d 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. ( dom F i^i ( x [,) +oo ) ) -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) <-> ( ( y e. B /\ x <_ y ) -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
38 impexp 
 |-  ( ( ( y e. B /\ x <_ y ) -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) <-> ( y e. B -> ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
39 37 38 bitrdi 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( ( y e. ( dom F i^i ( x [,) +oo ) ) -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) <-> ( y e. B -> ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) ) )
40 39 ralbidv2 
 |-  ( ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) /\ m e. RR ) -> ( A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) <-> A. y e. B ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
41 40 rexbidva 
 |-  ( ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) /\ x e. RR ) -> ( E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) <-> E. m e. RR A. y e. B ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
42 41 rexbidva 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) <-> E. x e. RR E. m e. RR A. y e. B ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
43 21 42 bitrd 
 |-  ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( F e. ( _O ` G ) <-> E. x e. RR E. m e. RR A. y e. B ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )