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
|
syl5bb |
|- ( ( ( 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
|
syl5bb |
|- ( ( ( ( ( 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 ) ) ) ) ) |