Metamath Proof Explorer


Theorem suplesup2

Description: If any element of A is less than or equal to an element in B , then the supremum of A is less than or equal to the supremum of B . (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses suplesup2.a
|- ( ph -> A C_ RR* )
suplesup2.b
|- ( ph -> B C_ RR* )
suplesup2.c
|- ( ( ph /\ x e. A ) -> E. y e. B x <_ y )
Assertion suplesup2
|- ( ph -> sup ( A , RR* , < ) <_ sup ( B , RR* , < ) )

Proof

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* , < ) )