Step |
Hyp |
Ref |
Expression |
1 |
|
suplesup2.a |
|- ( ph -> A C_ RR* ) |
2 |
|
suplesup2.b |
|- ( ph -> B C_ RR* ) |
3 |
|
suplesup2.c |
|- ( ( ph /\ x e. A ) -> E. y e. B x <_ y ) |
4 |
1
|
sselda |
|- ( ( ph /\ x e. A ) -> x e. RR* ) |
5 |
4
|
3ad2ant1 |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> x e. RR* ) |
6 |
|
simp1l |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> ph ) |
7 |
|
simp2 |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> y e. B ) |
8 |
2
|
sselda |
|- ( ( ph /\ y e. B ) -> y e. RR* ) |
9 |
6 7 8
|
syl2anc |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> y e. RR* ) |
10 |
|
supxrcl |
|- ( B C_ RR* -> sup ( B , RR* , < ) e. RR* ) |
11 |
2 10
|
syl |
|- ( ph -> sup ( B , RR* , < ) e. RR* ) |
12 |
6 11
|
syl |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> sup ( B , RR* , < ) e. RR* ) |
13 |
|
simp3 |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> x <_ y ) |
14 |
2
|
adantr |
|- ( ( ph /\ y e. B ) -> B C_ RR* ) |
15 |
|
simpr |
|- ( ( ph /\ y e. B ) -> y e. B ) |
16 |
|
supxrub |
|- ( ( B C_ RR* /\ y e. B ) -> y <_ sup ( B , RR* , < ) ) |
17 |
14 15 16
|
syl2anc |
|- ( ( ph /\ y e. B ) -> y <_ sup ( B , RR* , < ) ) |
18 |
6 7 17
|
syl2anc |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> y <_ sup ( B , RR* , < ) ) |
19 |
5 9 12 13 18
|
xrletrd |
|- ( ( ( ph /\ x e. A ) /\ y e. B /\ x <_ y ) -> x <_ sup ( B , RR* , < ) ) |
20 |
19
|
3exp |
|- ( ( ph /\ x e. A ) -> ( y e. B -> ( x <_ y -> x <_ sup ( B , RR* , < ) ) ) ) |
21 |
20
|
rexlimdv |
|- ( ( ph /\ x e. A ) -> ( E. y e. B x <_ y -> x <_ sup ( B , RR* , < ) ) ) |
22 |
3 21
|
mpd |
|- ( ( ph /\ x e. A ) -> x <_ sup ( B , RR* , < ) ) |
23 |
22
|
ralrimiva |
|- ( ph -> A. x e. A x <_ sup ( B , RR* , < ) ) |
24 |
|
supxrleub |
|- ( ( A C_ RR* /\ sup ( B , RR* , < ) e. RR* ) -> ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) <-> A. x e. A x <_ sup ( B , RR* , < ) ) ) |
25 |
1 11 24
|
syl2anc |
|- ( ph -> ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) <-> A. x e. A x <_ sup ( B , RR* , < ) ) ) |
26 |
23 25
|
mpbird |
|- ( ph -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) |