Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( ph /\ ps ) -> ph ) |
2 |
1
|
imim2i |
|- ( ( j <_ k -> ( ph /\ ps ) ) -> ( j <_ k -> ph ) ) |
3 |
2
|
ralimi |
|- ( A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> A. k e. A ( j <_ k -> ph ) ) |
4 |
3
|
reximi |
|- ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ph ) ) |
5 |
|
simpr |
|- ( ( ph /\ ps ) -> ps ) |
6 |
5
|
imim2i |
|- ( ( j <_ k -> ( ph /\ ps ) ) -> ( j <_ k -> ps ) ) |
7 |
6
|
ralimi |
|- ( A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> A. k e. A ( j <_ k -> ps ) ) |
8 |
7
|
reximi |
|- ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ps ) ) |
9 |
4 8
|
jca |
|- ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) -> ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) ) |
10 |
|
breq1 |
|- ( j = x -> ( j <_ k <-> x <_ k ) ) |
11 |
10
|
imbi1d |
|- ( j = x -> ( ( j <_ k -> ph ) <-> ( x <_ k -> ph ) ) ) |
12 |
11
|
ralbidv |
|- ( j = x -> ( A. k e. A ( j <_ k -> ph ) <-> A. k e. A ( x <_ k -> ph ) ) ) |
13 |
12
|
cbvrexvw |
|- ( E. j e. RR A. k e. A ( j <_ k -> ph ) <-> E. x e. RR A. k e. A ( x <_ k -> ph ) ) |
14 |
|
breq1 |
|- ( j = y -> ( j <_ k <-> y <_ k ) ) |
15 |
14
|
imbi1d |
|- ( j = y -> ( ( j <_ k -> ps ) <-> ( y <_ k -> ps ) ) ) |
16 |
15
|
ralbidv |
|- ( j = y -> ( A. k e. A ( j <_ k -> ps ) <-> A. k e. A ( y <_ k -> ps ) ) ) |
17 |
16
|
cbvrexvw |
|- ( E. j e. RR A. k e. A ( j <_ k -> ps ) <-> E. y e. RR A. k e. A ( y <_ k -> ps ) ) |
18 |
13 17
|
anbi12i |
|- ( ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) <-> ( E. x e. RR A. k e. A ( x <_ k -> ph ) /\ E. y e. RR A. k e. A ( y <_ k -> ps ) ) ) |
19 |
|
reeanv |
|- ( E. x e. RR E. y e. RR ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) <-> ( E. x e. RR A. k e. A ( x <_ k -> ph ) /\ E. y e. RR A. k e. A ( y <_ k -> ps ) ) ) |
20 |
18 19
|
bitr4i |
|- ( ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) <-> E. x e. RR E. y e. RR ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) ) |
21 |
|
ifcl |
|- ( ( y e. RR /\ x e. RR ) -> if ( x <_ y , y , x ) e. RR ) |
22 |
21
|
ancoms |
|- ( ( x e. RR /\ y e. RR ) -> if ( x <_ y , y , x ) e. RR ) |
23 |
22
|
adantl |
|- ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> if ( x <_ y , y , x ) e. RR ) |
24 |
|
r19.26 |
|- ( A. k e. A ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) <-> ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) ) |
25 |
|
anim12 |
|- ( ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) -> ( ( x <_ k /\ y <_ k ) -> ( ph /\ ps ) ) ) |
26 |
|
simplrl |
|- ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> x e. RR ) |
27 |
|
simplrr |
|- ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> y e. RR ) |
28 |
|
simpl |
|- ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> A C_ RR ) |
29 |
28
|
sselda |
|- ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> k e. RR ) |
30 |
|
maxle |
|- ( ( x e. RR /\ y e. RR /\ k e. RR ) -> ( if ( x <_ y , y , x ) <_ k <-> ( x <_ k /\ y <_ k ) ) ) |
31 |
26 27 29 30
|
syl3anc |
|- ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> ( if ( x <_ y , y , x ) <_ k <-> ( x <_ k /\ y <_ k ) ) ) |
32 |
31
|
imbi1d |
|- ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> ( ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) <-> ( ( x <_ k /\ y <_ k ) -> ( ph /\ ps ) ) ) ) |
33 |
25 32
|
syl5ibr |
|- ( ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) /\ k e. A ) -> ( ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) -> ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) ) |
34 |
33
|
ralimdva |
|- ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> ( A. k e. A ( ( x <_ k -> ph ) /\ ( y <_ k -> ps ) ) -> A. k e. A ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) ) |
35 |
24 34
|
syl5bir |
|- ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> ( ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) -> A. k e. A ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) ) |
36 |
|
breq1 |
|- ( j = if ( x <_ y , y , x ) -> ( j <_ k <-> if ( x <_ y , y , x ) <_ k ) ) |
37 |
36
|
rspceaimv |
|- ( ( if ( x <_ y , y , x ) e. RR /\ A. k e. A ( if ( x <_ y , y , x ) <_ k -> ( ph /\ ps ) ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) ) |
38 |
23 35 37
|
syl6an |
|- ( ( A C_ RR /\ ( x e. RR /\ y e. RR ) ) -> ( ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) ) ) |
39 |
38
|
rexlimdvva |
|- ( A C_ RR -> ( E. x e. RR E. y e. RR ( A. k e. A ( x <_ k -> ph ) /\ A. k e. A ( y <_ k -> ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) ) ) |
40 |
20 39
|
syl5bi |
|- ( A C_ RR -> ( ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) -> E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) ) ) |
41 |
9 40
|
impbid2 |
|- ( A C_ RR -> ( E. j e. RR A. k e. A ( j <_ k -> ( ph /\ ps ) ) <-> ( E. j e. RR A. k e. A ( j <_ k -> ph ) /\ E. j e. RR A. k e. A ( j <_ k -> ps ) ) ) ) |