Theorem xrsupss 6035

Description: Any subset of extended reals has a supremum.

Assertion

Ref	Expression
xrsupss	|- (A (_ RR* -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)))

Distinct variable group:   x,y,z,A

Proof of Theorem xrsupss

Step	Hyp	Ref	Expression
1		ssxr 5523	. . 3 |- (A (_ RR* -> (A (_ RR \/ +oo e. A \/ -oo e. A))
2		df-3or 775	. . 3 |- ((A (_ RR \/ +oo e. A \/ -oo e. A) <-> ((A (_ RR \/ +oo e. A) \/ -oo e. A))
3	1, 2	sylib 198	. 2 |- (A (_ RR* -> ((A (_ RR \/ +oo e. A) \/ -oo e. A))
4		xrsupsslem 6033	. . 3 |- ((A (_ RR* /\ (A (_ RR \/ +oo e. A)) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)))
5		ssdifss 2165	. . . . . 6 |- (A (_ RR* -> (A \ { -oo}) (_ RR*)
6		ssxr 5523	. . . . . . . 8 |- ((A \ { -oo}) (_ RR* -> ((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo}) \/ -oo e. (A \ { -oo})))
7		orcom 246	. . . . . . . . 9 |- ((((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo})) \/ -oo e. (A \ { -oo})) <-> ( -oo e. (A \ { -oo}) \/ ((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo}))))
8		df-3or 775	. . . . . . . . 9 |- (((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo}) \/ -oo e. (A \ { -oo})) <-> (((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo})) \/ -oo e. (A \ { -oo})))
9		mnfxr 5477	. . . . . . . . . . . . 13 |- -oo e. RR*
10	9	elisseti 1815	. . . . . . . . . . . 12 |- -oo e. V
11	10	snid 2432	. . . . . . . . . . 11 |- -oo e. { -oo}
12		elndif 2161	. . . . . . . . . . 11 |- ( -oo e. { -oo} -> -. -oo e. (A \ { -oo}))
13	11, 12	ax-mp 7	. . . . . . . . . 10 |- -. -oo e. (A \ { -oo})
14		biorf 734	. . . . . . . . . 10 |- (-. -oo e. (A \ { -oo}) -> (((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo})) <-> ( -oo e. (A \ { -oo}) \/ ((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo})))))
15	13, 14	ax-mp 7	. . . . . . . . 9 |- (((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo})) <-> ( -oo e. (A \ { -oo}) \/ ((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo}))))
16	7, 8, 15	3bitr4 183	. . . . . . . 8 |- (((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo}) \/ -oo e. (A \ { -oo})) <-> ((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo})))
17	6, 16	sylib 198	. . . . . . 7 |- ((A \ { -oo}) (_ RR* -> ((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo})))
18		xrsupsslem 6033	. . . . . . 7 |- (((A \ { -oo}) (_ RR* /\ ((A \ { -oo}) (_ RR \/ +oo e. (A \ { -oo}))) -> E.x e. RR* (A.y e. (A \ { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. (A \ { -oo})y < z)))
19	17, 18	mpdan 703	. . . . . 6 |- ((A \ { -oo}) (_ RR* -> E.x e. RR* (A.y e. (A \ { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. (A \ { -oo})y < z)))
20	5, 19	syl 10	. . . . 5 |- (A (_ RR* -> E.x e. RR* (A.y e. (A \ { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. (A \ { -oo})y < z)))
21	20	adantr 389	. . . 4 |- ((A (_ RR* /\ -oo e. A) -> E.x e. RR* (A.y e. (A \ { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. (A \ { -oo})y < z)))
22	10	snss 2458	. . . . . . . . 9 |- ( -oo e. A <-> { -oo} (_ A)
23		undif 2340	. . . . . . . . 9 |- ({ -oo} (_ A <-> ({ -oo} u. (A \ { -oo})) = A)
24		uncom 2173	. . . . . . . . . 10 |- ({ -oo} u. (A \ { -oo})) = ((A \ { -oo}) u. { -oo})
25	24	eqeq1i 1480	. . . . . . . . 9 |- (({ -oo} u. (A \ { -oo})) = A <-> ((A \ { -oo}) u. { -oo}) = A)
26	22, 23, 25	3bitr 177	. . . . . . . 8 |- ( -oo e. A <-> ((A \ { -oo}) u. { -oo}) = A)
27		raleq1 1784	. . . . . . . . 9 |- (((A \ { -oo}) u. { -oo}) = A -> (A.y e. ((A \ { -oo}) u. { -oo}) -. x < y <-> A.y e. A -. x < y))
28		rexeq1 1785	. . . . . . . . . . 11 |- (((A \ { -oo}) u. { -oo}) = A -> (E.z e. ((A \ { -oo}) u. { -oo})y < z <-> E.z e. A y < z))
29	28	imbi2d 611	. . . . . . . . . 10 |- (((A \ { -oo}) u. { -oo}) = A -> ((y < x -> E.z e. ((A \ { -oo}) u. { -oo})y < z) <-> (y < x -> E.z e. A y < z)))
30	29	ralbidv 1661	. . . . . . . . 9 |- (((A \ { -oo}) u. { -oo}) = A -> (A.y e. RR* (y < x -> E.z e. ((A \ { -oo}) u. { -oo})y < z) <-> A.y e. RR* (y < x -> E.z e. A y < z)))
31	27, 30	anbi12d 627	. . . . . . . 8 |- (((A \ { -oo}) u. { -oo}) = A -> ((A.y e. ((A \ { -oo}) u. { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. ((A \ { -oo}) u. { -oo})y < z)) <-> (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
32	26, 31	sylbi 199	. . . . . . 7 |- ( -oo e. A -> ((A.y e. ((A \ { -oo}) u. { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. ((A \ { -oo}) u. { -oo})y < z)) <-> (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
33	32	rexbidv 1662	. . . . . 6 |- ( -oo e. A -> (E.x e. RR* (A.y e. ((A \ { -oo}) u. { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. ((A \ { -oo}) u. { -oo})y < z)) <-> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
34		xrsupexmnf 6031	. . . . . 6 |- (E.x e. RR* (A.y e. (A \ { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. (A \ { -oo})y < z)) -> E.x e. RR* (A.y e. ((A \ { -oo}) u. { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. ((A \ { -oo}) u. { -oo})y < z)))
35	33, 34	syl5bi 208	. . . . 5 |- ( -oo e. A -> (E.x e. RR* (A.y e. (A \ { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. (A \ { -oo})y < z)) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
36	35	adantl 388	. . . 4 |- ((A (_ RR* /\ -oo e. A) -> (E.x e. RR* (A.y e. (A \ { -oo}) -. x < y /\ A.y e. RR* (y < x -> E.z e. (A \ { -oo})y < z)) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z))))
37	21, 36	mpd 26	. . 3 |- ((A (_ RR* /\ -oo e. A) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)))
38	4, 37	jaodan 426	. 2 |- ((A (_ RR* /\ ((A (_ RR \/ +oo e. A) \/ -oo e. A)) -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)))
39	3, 38	mpdan 703	1 |- (A (_ RR* -> E.x e. RR* (A.y e. A -. x < y /\ A.y e. RR* (y < x -> E.z e. A y < z)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   \/ w3o 773   = wceq 955   e. wcel 957  A.wral 1643  E.wrex 1644   \ cdif 2041   u. cun 2042   (_ wss 2044  {csn 2406   class class class wbr 2615  RRcr 5216   +oocpnf 5466   -oocmnf 5467  RR*cxr 5468   < clt 5469

This theorem is referenced by:  supxr 6038  supxrcl 6041  supxrun 6042  supxrunb1 6046  supxrunb2 6047  supxrub 6055  supxrleub 6056

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862  ax-inf2 4608

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex