Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( A C_ RR /\ B e. RR ) -> B e. RR ) |
2 |
|
pnfxr |
|- +oo e. RR* |
3 |
|
icossre |
|- ( ( B e. RR /\ +oo e. RR* ) -> ( B [,) +oo ) C_ RR ) |
4 |
1 2 3
|
sylancl |
|- ( ( A C_ RR /\ B e. RR ) -> ( B [,) +oo ) C_ RR ) |
5 |
|
ssrexv |
|- ( ( B [,) +oo ) C_ RR -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) -> E. j e. RR A. k e. A ( j <_ k -> ph ) ) ) |
6 |
4 5
|
syl |
|- ( ( A C_ RR /\ B e. RR ) -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) -> E. j e. RR A. k e. A ( j <_ k -> ph ) ) ) |
7 |
|
simpr |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> j e. RR ) |
8 |
|
simplr |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> B e. RR ) |
9 |
7 8
|
ifcld |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> if ( B <_ j , j , B ) e. RR ) |
10 |
|
max1 |
|- ( ( B e. RR /\ j e. RR ) -> B <_ if ( B <_ j , j , B ) ) |
11 |
10
|
adantll |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> B <_ if ( B <_ j , j , B ) ) |
12 |
|
elicopnf |
|- ( B e. RR -> ( if ( B <_ j , j , B ) e. ( B [,) +oo ) <-> ( if ( B <_ j , j , B ) e. RR /\ B <_ if ( B <_ j , j , B ) ) ) ) |
13 |
12
|
ad2antlr |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> ( if ( B <_ j , j , B ) e. ( B [,) +oo ) <-> ( if ( B <_ j , j , B ) e. RR /\ B <_ if ( B <_ j , j , B ) ) ) ) |
14 |
9 11 13
|
mpbir2and |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> if ( B <_ j , j , B ) e. ( B [,) +oo ) ) |
15 |
|
simpllr |
|- ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> B e. RR ) |
16 |
|
simplr |
|- ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> j e. RR ) |
17 |
|
simpll |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> A C_ RR ) |
18 |
17
|
sselda |
|- ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> k e. RR ) |
19 |
|
maxle |
|- ( ( B e. RR /\ j e. RR /\ k e. RR ) -> ( if ( B <_ j , j , B ) <_ k <-> ( B <_ k /\ j <_ k ) ) ) |
20 |
15 16 18 19
|
syl3anc |
|- ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> ( if ( B <_ j , j , B ) <_ k <-> ( B <_ k /\ j <_ k ) ) ) |
21 |
|
simpr |
|- ( ( B <_ k /\ j <_ k ) -> j <_ k ) |
22 |
20 21
|
syl6bi |
|- ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> ( if ( B <_ j , j , B ) <_ k -> j <_ k ) ) |
23 |
22
|
imim1d |
|- ( ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) /\ k e. A ) -> ( ( j <_ k -> ph ) -> ( if ( B <_ j , j , B ) <_ k -> ph ) ) ) |
24 |
23
|
ralimdva |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> ( A. k e. A ( j <_ k -> ph ) -> A. k e. A ( if ( B <_ j , j , B ) <_ k -> ph ) ) ) |
25 |
|
breq1 |
|- ( n = if ( B <_ j , j , B ) -> ( n <_ k <-> if ( B <_ j , j , B ) <_ k ) ) |
26 |
25
|
rspceaimv |
|- ( ( if ( B <_ j , j , B ) e. ( B [,) +oo ) /\ A. k e. A ( if ( B <_ j , j , B ) <_ k -> ph ) ) -> E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) ) |
27 |
14 24 26
|
syl6an |
|- ( ( ( A C_ RR /\ B e. RR ) /\ j e. RR ) -> ( A. k e. A ( j <_ k -> ph ) -> E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) ) ) |
28 |
27
|
rexlimdva |
|- ( ( A C_ RR /\ B e. RR ) -> ( E. j e. RR A. k e. A ( j <_ k -> ph ) -> E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) ) ) |
29 |
|
breq1 |
|- ( n = j -> ( n <_ k <-> j <_ k ) ) |
30 |
29
|
imbi1d |
|- ( n = j -> ( ( n <_ k -> ph ) <-> ( j <_ k -> ph ) ) ) |
31 |
30
|
ralbidv |
|- ( n = j -> ( A. k e. A ( n <_ k -> ph ) <-> A. k e. A ( j <_ k -> ph ) ) ) |
32 |
31
|
cbvrexvw |
|- ( E. n e. ( B [,) +oo ) A. k e. A ( n <_ k -> ph ) <-> E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) ) |
33 |
28 32
|
syl6ib |
|- ( ( A C_ RR /\ B e. RR ) -> ( E. j e. RR A. k e. A ( j <_ k -> ph ) -> E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) ) ) |
34 |
6 33
|
impbid |
|- ( ( A C_ RR /\ B e. RR ) -> ( E. j e. ( B [,) +oo ) A. k e. A ( j <_ k -> ph ) <-> E. j e. RR A. k e. A ( j <_ k -> ph ) ) ) |