Step |
Hyp |
Ref |
Expression |
1 |
|
supicc.1 |
|- ( ph -> B e. RR ) |
2 |
|
supicc.2 |
|- ( ph -> C e. RR ) |
3 |
|
supicc.3 |
|- ( ph -> A C_ ( B [,] C ) ) |
4 |
|
supicc.4 |
|- ( ph -> A =/= (/) ) |
5 |
|
supiccub.1 |
|- ( ph -> D e. A ) |
6 |
|
iccssre |
|- ( ( B e. RR /\ C e. RR ) -> ( B [,] C ) C_ RR ) |
7 |
1 2 6
|
syl2anc |
|- ( ph -> ( B [,] C ) C_ RR ) |
8 |
3 7
|
sstrd |
|- ( ph -> A C_ RR ) |
9 |
1
|
adantr |
|- ( ( ph /\ x e. A ) -> B e. RR ) |
10 |
9
|
rexrd |
|- ( ( ph /\ x e. A ) -> B e. RR* ) |
11 |
2
|
adantr |
|- ( ( ph /\ x e. A ) -> C e. RR ) |
12 |
11
|
rexrd |
|- ( ( ph /\ x e. A ) -> C e. RR* ) |
13 |
3
|
sselda |
|- ( ( ph /\ x e. A ) -> x e. ( B [,] C ) ) |
14 |
|
iccleub |
|- ( ( B e. RR* /\ C e. RR* /\ x e. ( B [,] C ) ) -> x <_ C ) |
15 |
10 12 13 14
|
syl3anc |
|- ( ( ph /\ x e. A ) -> x <_ C ) |
16 |
15
|
ralrimiva |
|- ( ph -> A. x e. A x <_ C ) |
17 |
|
brralrspcev |
|- ( ( C e. RR /\ A. x e. A x <_ C ) -> E. y e. RR A. x e. A x <_ y ) |
18 |
2 16 17
|
syl2anc |
|- ( ph -> E. y e. RR A. x e. A x <_ y ) |
19 |
8 4 18 5
|
suprubd |
|- ( ph -> D <_ sup ( A , RR , < ) ) |