Theorem supxrun 6040

Description: The supremum of the union of two sets of extended reals equals the largest of their suprema.

Assertion

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

Proof of Theorem supxrun

Step	Hyp	Ref	Expression
1		supxr 6036	. 2 |- ((((A u. B) (_ 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*, < ))
2		unss 2200	. . . 4 |- ((A (_ RR* /\ B (_ RR*) <-> (A u. B) (_ RR*)
3	2	biimp 151	. . 3 |- ((A (_ RR* /\ B (_ RR*) -> (A u. B) (_ RR*)
4	3	3adant3 798	. 2 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (A u. B) (_ RR*)
5		supxrcl 6039	. . 3 |- (B (_ RR* -> sup(B, RR*, < ) e. RR*)
6	5	3ad2ant2 800	. 2 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> sup(B, RR*, < ) e. RR*)
7		xrsupss 6033	. . . . . . . 8 |- (A (_ RR* -> E.y e. RR* (A.z e. A -. y < z /\ A.z e. RR* (z < y -> E.w e. A z < w)))
8		xrltso 5535	. . . . . . . . 9 |- < Or RR*
9	8	supub 4560	. . . . . . . 8 |- (E.y e. RR* (A.z e. A -. y < z /\ A.z e. RR* (z < y -> E.w e. A z < w)) -> (x e. A -> -. sup(A, RR*, < ) < x))
10	7, 9	syl 10	. . . . . . 7 |- (A (_ RR* -> (x e. A -> -. sup(A, RR*, < ) < x))
11	10	3ad2ant1 799	. . . . . 6 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. A -> -. sup(A, RR*, < ) < x))
12		xrlelttrt 5543	. . . . . . . . . . . . 13 |- ((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))
13		supxrcl 6039	. . . . . . . . . . . . . 14 |- (A (_ RR* -> sup(A, RR*, < ) e. RR*)
14	13	ad2antrr 404	. . . . . . . . . . . . 13 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> sup(A, RR*, < ) e. RR*)
15	5	ad2antlr 405	. . . . . . . . . . . . 13 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> sup(B, RR*, < ) e. RR*)
16		ssel2 2060	. . . . . . . . . . . . . 14 |- ((A (_ RR* /\ x e. A) -> x e. RR*)
17	16	adantlr 393	. . . . . . . . . . . . 13 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> x e. RR*)
18	12, 14, 15, 17	syl3anc 857	. . . . . . . . . . . 12 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> ((sup(A, RR*, < ) <_ sup(B, RR*, < ) /\ sup(B, RR*, < ) < x) -> sup(A, RR*, < ) < x))
19	18	exp3a 375	. . . . . . . . . . 11 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> (sup(A, RR*, < ) <_ sup(B, RR*, < ) -> (sup(B, RR*, < ) < x -> sup(A, RR*, < ) < x)))
20	19	imp 350	. . . . . . . . . 10 |- ((((A (_ RR* /\ B (_ RR*) /\ x e. A) /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (sup(B, RR*, < ) < x -> sup(A, RR*, < ) < x))
21	20	con3d 95	. . . . . . . . 9 |- ((((A (_ RR* /\ B (_ RR*) /\ x e. A) /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x))
22	21	exp41 382	. . . . . . . 8 |- (A (_ RR* -> (B (_ RR* -> (x e. A -> (sup(A, RR*, < ) <_ sup(B, RR*, < ) -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x)))))
23	22	com34 36	. . . . . . 7 |- (A (_ RR* -> (B (_ RR* -> (sup(A, RR*, < ) <_ sup(B, RR*, < ) -> (x e. A -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x)))))
24	23	3imp 826	. . . . . 6 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. A -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x)))
25	11, 24	mpdd 46	. . . . 5 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. A -> -. sup(B, RR*, < ) < x))
26		xrsupss 6033	. . . . . . 7 |- (B (_ RR* -> E.y e. RR* (A.z e. B -. y < z /\ A.z e. RR* (z < y -> E.w e. B z < w)))
27	8	supub 4560	. . . . . . 7 |- (E.y e. RR* (A.z e. B -. y < z /\ A.z e. RR* (z < y -> E.w e. B z < w)) -> (x e. B -> -. sup(B, RR*, < ) < x))
28	26, 27	syl 10	. . . . . 6 |- (B (_ RR* -> (x e. B -> -. sup(B, RR*, < ) < x))
29	28	3ad2ant2 800	. . . . 5 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. B -> -. sup(B, RR*, < ) < x))
30	25, 29	jaod 424	. . . 4 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> ((x e. A \/ x e. B) -> -. sup(B, RR*, < ) < x))
31		elun 2169	. . . 4 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
32	30, 31	syl5ib 206	. . 3 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. (A u. B) -> -. sup(B, RR*, < ) < x))
33	32	r19.21aiv 1710	. 2 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> A.x e. (A u. B) -. sup(B, RR*, < ) < x)
34		xrsupss 6033	. . . . . . 7 |- (B (_ RR* -> E.x e. RR* (A.z e. B -. x < z /\ A.z e. RR* (z < x -> E.y e. B z < y)))
35	8	suplub 4561	. . . . . . . 8 |- (E.x e. RR* (A.z e. B -. x < z /\ A.z e. RR* (z < x -> E.y e. B z < y)) -> ((x e. RR* /\ x < sup(B, RR*, < )) -> E.y e. B x < y))
36		rexrt 5479	. . . . . . . 8 |- (x e. RR -> x e. RR*)
37	35, 36	sylani 464	. . . . . . 7 |- (E.x e. RR* (A.z e. B -. x < z /\ A.z e. RR* (z < x -> E.y e. B z < y)) -> ((x e. RR /\ x < sup(B, RR*, < )) -> E.y e. B x < y))
38	34, 37	syl 10	. . . . . 6 |- (B (_ RR* -> ((x e. RR /\ x < sup(B, RR*, < )) -> E.y e. B x < y))
39		elun2 2194	. . . . . . . 8 |- (y e. B -> y e. (A u. B))
40	39	anim1i 334	. . . . . . 7 |- ((y e. B /\ x < y) -> (y e. (A u. B) /\ x < y))
41	40	r19.22i2 1730	. . . . . 6 |- (E.y e. B x < y -> E.y e. (A u. B)x < y)
42	38, 41	syl6 22	. . . . 5 |- (B (_ RR* -> ((x e. RR /\ x < sup(B, RR*, < )) -> E.y e. (A u. B)x < y))
43	42	exp3a 375	. . . 4 |- (B (_ RR* -> (x e. RR -> (x < sup(B, RR*, < ) -> E.y e. (A u. B)x < y)))
44	43	r19.21aiv 1710	. . 3 |- (B (_ RR* -> A.x e. RR (x < sup(B, RR*, < ) -> E.y e. (A u. B)x < y))
45	44	3ad2ant2 800	. 2 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> A.x e. RR (x < sup(B, RR*, < ) -> E.y e. (A u. B)x < y))
46	1, 4, 6, 33, 45	syl2anc 472	1 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> sup((A u. B), RR*, < ) = sup(B, RR*, < ))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223   /\ w3a 774   = wceq 954   e. wcel 956  A.wral 1642  E.wrex 1643   u. cun 2041   (_ wss 2043   class class class wbr 2614  supcsup 4553  RRcr 5213   <_ cle 5275  RR*cxr 5465   < clt 5466

This theorem is referenced by:  supxrmnf 6042

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o