Step |
Hyp |
Ref |
Expression |
1 |
|
lo1resb.1 |
|- ( ph -> F : A --> RR ) |
2 |
|
lo1resb.2 |
|- ( ph -> A C_ RR ) |
3 |
|
lo1resb.3 |
|- ( ph -> B e. RR ) |
4 |
|
lo1res |
|- ( F e. <_O(1) -> ( F |` ( B [,) +oo ) ) e. <_O(1) ) |
5 |
1
|
feqmptd |
|- ( ph -> F = ( x e. A |-> ( F ` x ) ) ) |
6 |
5
|
reseq1d |
|- ( ph -> ( F |` ( B [,) +oo ) ) = ( ( x e. A |-> ( F ` x ) ) |` ( B [,) +oo ) ) ) |
7 |
|
resmpt3 |
|- ( ( x e. A |-> ( F ` x ) ) |` ( B [,) +oo ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) |
8 |
6 7
|
eqtrdi |
|- ( ph -> ( F |` ( B [,) +oo ) ) = ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) ) |
9 |
8
|
eleq1d |
|- ( ph -> ( ( F |` ( B [,) +oo ) ) e. <_O(1) <-> ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) e. <_O(1) ) ) |
10 |
|
inss1 |
|- ( A i^i ( B [,) +oo ) ) C_ A |
11 |
10 2
|
sstrid |
|- ( ph -> ( A i^i ( B [,) +oo ) ) C_ RR ) |
12 |
|
elinel1 |
|- ( x e. ( A i^i ( B [,) +oo ) ) -> x e. A ) |
13 |
|
ffvelrn |
|- ( ( F : A --> RR /\ x e. A ) -> ( F ` x ) e. RR ) |
14 |
1 12 13
|
syl2an |
|- ( ( ph /\ x e. ( A i^i ( B [,) +oo ) ) ) -> ( F ` x ) e. RR ) |
15 |
11 14
|
ello1mpt |
|- ( ph -> ( ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) e. <_O(1) <-> E. y e. RR E. z e. RR A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) ) ) |
16 |
|
elin |
|- ( x e. ( A i^i ( B [,) +oo ) ) <-> ( x e. A /\ x e. ( B [,) +oo ) ) ) |
17 |
16
|
imbi1i |
|- ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( ( x e. A /\ x e. ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) |
18 |
|
impexp |
|- ( ( ( x e. A /\ x e. ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( x e. A -> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) ) |
19 |
17 18
|
bitri |
|- ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( x e. A -> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) ) |
20 |
|
impexp |
|- ( ( ( x e. ( B [,) +oo ) /\ y <_ x ) -> ( F ` x ) <_ z ) <-> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) |
21 |
3
|
ad2antrr |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> B e. RR ) |
22 |
2
|
adantr |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> A C_ RR ) |
23 |
22
|
sselda |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> x e. RR ) |
24 |
|
elicopnf |
|- ( B e. RR -> ( x e. ( B [,) +oo ) <-> ( x e. RR /\ B <_ x ) ) ) |
25 |
24
|
baibd |
|- ( ( B e. RR /\ x e. RR ) -> ( x e. ( B [,) +oo ) <-> B <_ x ) ) |
26 |
21 23 25
|
syl2anc |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( x e. ( B [,) +oo ) <-> B <_ x ) ) |
27 |
26
|
anbi1d |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( x e. ( B [,) +oo ) /\ y <_ x ) <-> ( B <_ x /\ y <_ x ) ) ) |
28 |
|
simplrl |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> y e. RR ) |
29 |
|
maxle |
|- ( ( B e. RR /\ y e. RR /\ x e. RR ) -> ( if ( B <_ y , y , B ) <_ x <-> ( B <_ x /\ y <_ x ) ) ) |
30 |
21 28 23 29
|
syl3anc |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( if ( B <_ y , y , B ) <_ x <-> ( B <_ x /\ y <_ x ) ) ) |
31 |
27 30
|
bitr4d |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( x e. ( B [,) +oo ) /\ y <_ x ) <-> if ( B <_ y , y , B ) <_ x ) ) |
32 |
31
|
imbi1d |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( ( x e. ( B [,) +oo ) /\ y <_ x ) -> ( F ` x ) <_ z ) <-> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) ) |
33 |
20 32
|
bitr3id |
|- ( ( ( ph /\ ( y e. RR /\ z e. RR ) ) /\ x e. A ) -> ( ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) ) |
34 |
33
|
pm5.74da |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( ( x e. A -> ( x e. ( B [,) +oo ) -> ( y <_ x -> ( F ` x ) <_ z ) ) ) <-> ( x e. A -> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) ) ) |
35 |
19 34
|
syl5bb |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( ( x e. ( A i^i ( B [,) +oo ) ) -> ( y <_ x -> ( F ` x ) <_ z ) ) <-> ( x e. A -> ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) ) ) |
36 |
35
|
ralbidv2 |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) <-> A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) ) |
37 |
1
|
adantr |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> F : A --> RR ) |
38 |
|
simprl |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> y e. RR ) |
39 |
3
|
adantr |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> B e. RR ) |
40 |
38 39
|
ifcld |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> if ( B <_ y , y , B ) e. RR ) |
41 |
|
simprr |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> z e. RR ) |
42 |
|
ello12r |
|- ( ( ( F : A --> RR /\ A C_ RR ) /\ ( if ( B <_ y , y , B ) e. RR /\ z e. RR ) /\ A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) ) -> F e. <_O(1) ) |
43 |
42
|
3expia |
|- ( ( ( F : A --> RR /\ A C_ RR ) /\ ( if ( B <_ y , y , B ) e. RR /\ z e. RR ) ) -> ( A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) ) |
44 |
37 22 40 41 43
|
syl22anc |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( A. x e. A ( if ( B <_ y , y , B ) <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) ) |
45 |
36 44
|
sylbid |
|- ( ( ph /\ ( y e. RR /\ z e. RR ) ) -> ( A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) ) |
46 |
45
|
rexlimdvva |
|- ( ph -> ( E. y e. RR E. z e. RR A. x e. ( A i^i ( B [,) +oo ) ) ( y <_ x -> ( F ` x ) <_ z ) -> F e. <_O(1) ) ) |
47 |
15 46
|
sylbid |
|- ( ph -> ( ( x e. ( A i^i ( B [,) +oo ) ) |-> ( F ` x ) ) e. <_O(1) -> F e. <_O(1) ) ) |
48 |
9 47
|
sylbid |
|- ( ph -> ( ( F |` ( B [,) +oo ) ) e. <_O(1) -> F e. <_O(1) ) ) |
49 |
4 48
|
impbid2 |
|- ( ph -> ( F e. <_O(1) <-> ( F |` ( B [,) +oo ) ) e. <_O(1) ) ) |