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