Theorem xrsupss 6025

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 5513	. . 3 |- (A (_ RR* -> (A (_ RR \/ +oo e. A \/ -oo e. A))
2		df-3or 774	. . 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 6023	. . 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 2158	. . . . . 6 |- (A (_ RR* -> (A \ { -oo}) (_ RR*)
6		ssxr 5513	. . . . . . . 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 774	. . . . . . . . 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 5466	. . . . . . . . . . . . 13 |- -oo e. RR*
10	9	elisseti 1809	. . . . . . . . . . . 12 |- -oo e. V
11	10	snid 2425	. . . . . . . . . . 11 |- -oo e. { -oo}
12		elndif 2154	. . . . . . . . . . 11 |- ( -oo e. { -oo} -> -. -oo e. (A \ { -oo}))
13	11, 12	ax-mp 7	. . . . . . . . . 10 |- -. -oo e. (A \ { -oo})
14		biorf 733	. . . . . . . . . 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 6023	. . . . . . 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 702	. . . . . 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 2452	. . . . . . . . 9 |- ( -oo e. A <-> { -oo} (_ A)
23		undif 2333	. . . . . . . . 9 |- ({ -oo} (_ A <-> ({ -oo} u. (A \ { -oo})) = A)
24		uncom 2166	. . . . . . . . . 10 |- ({ -oo} u. (A \ { -oo})) = ((A \ { -oo}) u. { -oo})
25	24	eqeq1i 1474	. . . . . . . . 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 1778	. . . . . . . . 9 |- (((A \ { -oo}) u. { -oo}) = A -> (A.y e. ((A \ { -oo}) u. { -oo}) -. x < y <-> A.y e. A -. x < y))
28		rexeq1 1779	. . . . . . . . . . 11 |- (((A \ { -oo}) u. { -oo}) = A -> (E.z e. ((A \ { -oo}) u. { -oo})y < z <-> E.z e. A y < z))
29	28	imbi2d 610	. . . . . . . . . 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 1655	. . . . . . . . 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 626	. . . . . . . 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 1656	. . . . . 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 6021	. . . . . 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 702	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 772   = wceq 953   e. wcel 955  A.wral 1637  E.wrex 1638   \ cdif 2034   u. cun 2035   (_ wss 2037  {csn 2399   class class class wbr 2609  RRcr 5205   +oocpnf 5455   -oocmnf 5456  RR*cxr 5457   < clt 5458

This theorem is referenced by:  supxr 6028  supxrcl 6031  supxrun 6032  supxrunb1 6036  supxrunb2 6037  supxrub 6045  supxrleub 6046

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597

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