Metamath Proof Explorer

Theorem supxrun

Description: The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion supxrun 
|- ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> sup ( ( A u. B ) , RR* , < ) = sup ( B , RR* , < ) )

Proof

Step Hyp Ref Expression
1 unss 
 |-  ( ( A C_ RR* /\ B C_ RR* ) <-> ( A u. B ) C_ RR* )
2 1 biimpi 
 |-  ( ( A C_ RR* /\ B C_ RR* ) -> ( A u. B ) C_ RR* )
3 2 3adant3 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( A u. B ) C_ RR* )
4 supxrcl 
 |-  ( B C_ RR* -> sup ( B , RR* , < ) e. RR* )
5 4 3ad2ant2 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> sup ( B , RR* , < ) e. RR* )
6 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
7 xrltso 
 |-  < Or RR*
8 7 a1i 
 |-  ( A C_ RR* -> < Or RR* )
9 xrsupss 
 |-  ( A C_ RR* -> E. y e. RR* ( A. z e. A -. y < z /\ A. z e. RR* ( z < y -> E. w e. A z < w ) ) )
10 8 9 supub 
 |-  ( A C_ RR* -> ( x e. A -> -. sup ( A , RR* , < ) < x ) )
11 10 3ad2ant1 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( x e. A -> -. sup ( A , RR* , < ) < x ) )
12 supxrcl 
 |-  ( A C_ RR* -> sup ( A , RR* , < ) e. RR* )
13 12 ad2antrr 
 |-  ( ( ( A C_ RR* /\ B C_ RR* ) /\ x e. A ) -> sup ( A , RR* , < ) e. RR* )
14 4 ad2antlr 
 |-  ( ( ( A C_ RR* /\ B C_ RR* ) /\ x e. A ) -> sup ( B , RR* , < ) e. RR* )
15 ssel2 
 |-  ( ( A C_ RR* /\ x e. A ) -> x e. RR* )
16 15 adantlr 
 |-  ( ( ( A C_ RR* /\ B C_ RR* ) /\ x e. A ) -> x e. RR* )
17 xrlelttr 
 |-  ( ( sup ( A , RR* , < ) e. RR* /\ sup ( B , RR* , < ) e. RR* /\ x e. RR* ) -> ( ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) /\ sup ( B , RR* , < ) < x ) -> sup ( A , RR* , < ) < x ) )
18 13 14 16 17 syl3anc 
 |-  ( ( ( A C_ RR* /\ B C_ RR* ) /\ x e. A ) -> ( ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) /\ sup ( B , RR* , < ) < x ) -> sup ( A , RR* , < ) < x ) )
19 18 expdimp 
 |-  ( ( ( ( A C_ RR* /\ B C_ RR* ) /\ x e. A ) /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( sup ( B , RR* , < ) < x -> sup ( A , RR* , < ) < x ) )
20 19 con3d 
 |-  ( ( ( ( A C_ RR* /\ B C_ RR* ) /\ x e. A ) /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( -. sup ( A , RR* , < ) < x -> -. sup ( B , RR* , < ) < x ) )
21 20 exp41 
 |-  ( A C_ RR* -> ( B C_ RR* -> ( x e. A -> ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) -> ( -. sup ( A , RR* , < ) < x -> -. sup ( B , RR* , < ) < x ) ) ) ) )
22 21 com34 
 |-  ( A C_ RR* -> ( B C_ RR* -> ( sup ( A , RR* , < ) <_ sup ( B , RR* , < ) -> ( x e. A -> ( -. sup ( A , RR* , < ) < x -> -. sup ( B , RR* , < ) < x ) ) ) ) )
23 22 3imp 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( x e. A -> ( -. sup ( A , RR* , < ) < x -> -. sup ( B , RR* , < ) < x ) ) )
24 11 23 mpdd 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( x e. A -> -. sup ( B , RR* , < ) < x ) )
25 7 a1i 
 |-  ( B C_ RR* -> < Or RR* )
26 xrsupss 
 |-  ( B C_ RR* -> E. y e. RR* ( A. z e. B -. y < z /\ A. z e. RR* ( z < y -> E. w e. B z < w ) ) )
27 25 26 supub 
 |-  ( B C_ RR* -> ( x e. B -> -. sup ( B , RR* , < ) < x ) )
28 27 3ad2ant2 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( x e. B -> -. sup ( B , RR* , < ) < x ) )
29 24 28 jaod 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( ( x e. A \/ x e. B ) -> -. sup ( B , RR* , < ) < x ) )
30 6 29 syl5bi 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> ( x e. ( A u. B ) -> -. sup ( B , RR* , < ) < x ) )
31 30 ralrimiv 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> A. x e. ( A u. B ) -. sup ( B , RR* , < ) < x )
32 rexr 
 |-  ( x e. RR -> x e. RR* )
33 xrsupss 
 |-  ( B C_ RR* -> E. x e. RR* ( A. z e. B -. x < z /\ A. z e. RR* ( z < x -> E. y e. B z < y ) ) )
34 25 33 suplub 
 |-  ( B C_ RR* -> ( ( x e. RR* /\ x < sup ( B , RR* , < ) ) -> E. y e. B x < y ) )
35 32 34 sylani 
 |-  ( B C_ RR* -> ( ( x e. RR /\ x < sup ( B , RR* , < ) ) -> E. y e. B x < y ) )
36 elun2 
 |-  ( y e. B -> y e. ( A u. B ) )
37 36 anim1i 
 |-  ( ( y e. B /\ x < y ) -> ( y e. ( A u. B ) /\ x < y ) )
38 37 reximi2 
 |-  ( E. y e. B x < y -> E. y e. ( A u. B ) x < y )
39 35 38 syl6 
 |-  ( B C_ RR* -> ( ( x e. RR /\ x < sup ( B , RR* , < ) ) -> E. y e. ( A u. B ) x < y ) )
40 39 expd 
 |-  ( B C_ RR* -> ( x e. RR -> ( x < sup ( B , RR* , < ) -> E. y e. ( A u. B ) x < y ) ) )
41 40 ralrimiv 
 |-  ( B C_ RR* -> A. x e. RR ( x < sup ( B , RR* , < ) -> E. y e. ( A u. B ) x < y ) )
42 41 3ad2ant2 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> A. x e. RR ( x < sup ( B , RR* , < ) -> E. y e. ( A u. B ) x < y ) )
43 supxr 
 |-  ( ( ( ( A u. B ) C_ RR* /\ sup ( B , RR* , < ) e. RR* ) /\ ( A. x e. ( A u. B ) -. sup ( B , RR* , < ) < x /\ A. x e. RR ( x < sup ( B , RR* , < ) -> E. y e. ( A u. B ) x < y ) ) ) -> sup ( ( A u. B ) , RR* , < ) = sup ( B , RR* , < ) )
44 3 5 31 42 43 syl22anc 
 |-  ( ( A C_ RR* /\ B C_ RR* /\ sup ( A , RR* , < ) <_ sup ( B , RR* , < ) ) -> sup ( ( A u. B ) , RR* , < ) = sup ( B , RR* , < ) )