Theorem supxrun 6087

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 6083	. 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 2207	. . . 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 801	. 2 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (A u. B) (_ RR*)
5		supxrcl 6086	. . 3 |- (B (_ RR* -> sup(B, RR*, < ) e. RR*)
6	5	3ad2ant2 803	. 2 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> sup(B, RR*, < ) e. RR*)
7		xrsupss 6080	. . . . . . . 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 5566	. . . . . . . . 9 |- < Or RR*
9	8	supub 4589	. . . . . . . 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 802	. . . . . 6 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. A -> -. sup(A, RR*, < ) < x))
12		xrlelttrt 5574	. . . . . . . . . . . 12 |- ((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 6086	. . . . . . . . . . . . 13 |- (A (_ RR* -> sup(A, RR*, < ) e. RR*)
14	13	ad2antrr 406	. . . . . . . . . . . 12 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> sup(A, RR*, < ) e. RR*)
15	5	ad2antlr 407	. . . . . . . . . . . 12 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> sup(B, RR*, < ) e. RR*)
16		ssel2 2067	. . . . . . . . . . . . 13 |- ((A (_ RR* /\ x e. A) -> x e. RR*)
17	16	adantlr 395	. . . . . . . . . . . 12 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> x e. RR*)
18	12, 14, 15, 17	syl3anc 860	. . . . . . . . . . 11 |- (((A (_ RR* /\ B (_ RR*) /\ x e. A) -> ((sup(A, RR*, < ) <_ sup(B, RR*, < ) /\ sup(B, RR*, < ) < x) -> sup(A, RR*, < ) < x))
19	18	expdimp 377	. . . . . . . . . 10 |- ((((A (_ RR* /\ B (_ RR*) /\ x e. A) /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (sup(B, RR*, < ) < x -> sup(A, RR*, < ) < x))
20	19	con3d 95	. . . . . . . . 9 |- ((((A (_ RR* /\ B (_ RR*) /\ x e. A) /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x))
21	20	exp41 384	. . . . . . . 8 |- (A (_ RR* -> (B (_ RR* -> (x e. A -> (sup(A, RR*, < ) <_ sup(B, RR*, < ) -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x)))))
22	21	com34 36	. . . . . . 7 |- (A (_ RR* -> (B (_ RR* -> (sup(A, RR*, < ) <_ sup(B, RR*, < ) -> (x e. A -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x)))))
23	22	3imp 829	. . . . . 6 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. A -> (-. sup(A, RR*, < ) < x -> -. sup(B, RR*, < ) < x)))
24	11, 23	mpdd 46	. . . . 5 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. A -> -. sup(B, RR*, < ) < x))
25		xrsupss 6080	. . . . . . 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)))
26	8	supub 4589	. . . . . . 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))
27	25, 26	syl 10	. . . . . 6 |- (B (_ RR* -> (x e. B -> -. sup(B, RR*, < ) < x))
28	27	3ad2ant2 803	. . . . 5 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. B -> -. sup(B, RR*, < ) < x))
29	24, 28	jaod 426	. . . 4 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> ((x e. A \/ x e. B) -> -. sup(B, RR*, < ) < x))
30		elun 2176	. . . 4 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
31	29, 30	syl5ib 206	. . 3 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> (x e. (A u. B) -> -. sup(B, RR*, < ) < x))
32	31	r19.21aiv 1716	. 2 |- ((A (_ RR* /\ B (_ RR* /\ sup(A, RR*, < ) <_ sup(B, RR*, < )) -> A.x e. (A u. B) -. sup(B, RR*, < ) < x)
33		xrsupss 6080	. . . . . . 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)))
34	8	suplub 4590	. . . . . . . 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))
35		rexrt 5511	. . . . . . . 8 |- (x e. RR -> x e. RR*)
36	34, 35	sylani 466	. . . . . . 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))
37	33, 36	syl 10	. . . . . 6 |- (B (_ RR* -> ((x e. RR /\ x < sup(B, RR*, < )) -> E.y e. B x < y))
38		elun2 2201	. . . . . . . 8 |- (y e. B -> y e. (A u. B))
39	38	anim1i 334	. . . . . . 7 |- ((y e. B /\ x < y) -> (y e. (A u. B) /\ x < y))
40	39	r19.22i2 1736	. . . . . 6 |- (E.y e. B x < y -> E.y e. (A u. B)x < y)
41	37, 40	syl6 22	. . . . 5 |- (B (_ RR* -> ((x e. RR /\ x < sup(B, RR*, < )) -> E.y e. (A u. B)x < y))
42	41	exp3a 376	. . . 4 |- (B (_ RR* -> (x e. RR -> (x < sup(B, RR*, < ) -> E.y e. (A u. B)x < y)))
43	42	r19.21aiv 1716	. . 3 |- (B (_ RR* -> A.x e. RR (x < sup(B, RR*, < ) -> E.y e. (A u. B)x < y))
44	43	3ad2ant2 803	. 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))
45	1, 4, 6, 32, 44	syl2anc 474	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 777   = wceq 958   e. wcel 960  A.wral 1648  E.wrex 1649   u. cun 2048   (_ wss 2050   class class class wbr 2624  supcsup 4582  RRcr 5245   <_ cle 5307  RR*cxr 5497   < clt 5498

This theorem is referenced by:  supxrmnf 6089

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-nel 1591  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419 &