Theorem supminfxr 39694

Description: The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Hypothesis

Ref	Expression
supminfxr.1	|- ( ph -> A C_ RR )

Assertion

Ref	Expression
supminfxr	|- ( ph -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem supminfxr

Dummy variables v w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		supeq1 8351	. . . . 5 |- ( A = (/) -> sup ( A , RR* , < ) = sup ( (/) , RR* , < ) )
2		xrsup0 12153	. . . . . 6 |- sup ( (/) , RR* , < ) = -oo
3	2	a1i 11	. . . . 5 |- ( A = (/) -> sup ( (/) , RR* , < ) = -oo )
4	1, 3	eqtrd 2656	. . . 4 |- ( A = (/) -> sup ( A , RR* , < ) = -oo )
5	4	adantl 482	. . 3 |- ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) = -oo )
6		eleq2 2690	. . . . . . . . . 10 |- ( A = (/) -> ( -u x e. A <-> -u x e. (/) ) )
7	6	rabbidv 3189	. . . . . . . . 9 |- ( A = (/) -> { x e. RR | -u x e. A } = { x e. RR | -u x e. (/) } )
8		noel 3919	. . . . . . . . . . . . 13 |- -. -u x e. (/)
9	8	a1i 11	. . . . . . . . . . . 12 |- ( x e. RR -> -. -u x e. (/) )
10	9	rgen 2922	. . . . . . . . . . 11 |- A. x e. RR -. -u x e. (/)
11		rabeq0 3957	. . . . . . . . . . 11 |- ( { x e. RR | -u x e. (/) } = (/) <-> A. x e. RR -. -u x e. (/) )
12	10, 11	mpbir 221	. . . . . . . . . 10 |- { x e. RR | -u x e. (/) } = (/)
13	12	a1i 11	. . . . . . . . 9 |- ( A = (/) -> { x e. RR | -u x e. (/) } = (/) )
14	7, 13	eqtrd 2656	. . . . . . . 8 |- ( A = (/) -> { x e. RR | -u x e. A } = (/) )
15	14	infeq1d 8383	. . . . . . 7 |- ( A = (/) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = inf ( (/) , RR* , < ) )
16		xrinf0 12168	. . . . . . . 8 |- inf ( (/) , RR* , < ) = +oo
17	16	a1i 11	. . . . . . 7 |- ( A = (/) -> inf ( (/) , RR* , < ) = +oo )
18	15, 17	eqtrd 2656	. . . . . 6 |- ( A = (/) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = +oo )
19	18	xnegeqd 39664	. . . . 5 |- ( A = (/) -> -einf ( { x e. RR | -u x e. A } , RR* , < ) = -e +oo )
20		xnegpnf 12040	. . . . . 6 |- -e +oo = -oo
21	20	a1i 11	. . . . 5 |- ( A = (/) -> -e +oo = -oo )
22	19, 21	eqtrd 2656	. . . 4 |- ( A = (/) -> -einf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
23	22	adantl 482	. . 3 |- ( ( ph /\ A = (/) ) -> -einf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
24	5, 23	eqtr4d 2659	. 2 |- ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
25		neqne 2802	. . 3 |- ( -. A = (/) -> A =/= (/) )
26		supminfxr.1	. . . . . . 7 |- ( ph -> A C_ RR )
27	26	ad2antrr 762	. . . . . 6 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> A C_ RR )
28		simplr 792	. . . . . 6 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> A =/= (/) )
29		simpr 477	. . . . . 6 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> E. y e. RR A. z e. A z <_ y )
30		negn0 10459	. . . . . . . . . 10 |- ( ( A C_ RR /\ A =/= (/) ) -> { x e. RR | -u x e. A } =/= (/) )
31		ublbneg 11773	. . . . . . . . . 10 |- ( E. y e. RR A. z e. A z <_ y -> E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z )
32		ssrab2 3687	. . . . . . . . . . 11 |- { x e. RR | -u x e. A } C_ RR
33		infrenegsup 11006	. . . . . . . . . . 11 |- ( ( { x e. RR | -u x e. A } C_ RR /\ { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
34	32, 33	mp3an1 1411	. . . . . . . . . 10 |- ( ( { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
35	30, 31, 34	syl2an 494	. . . . . . . . 9 |- ( ( ( A C_ RR /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
36	35	3impa 1259	. . . . . . . 8 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) )
37		elrabi 3359	. . . . . . . . . . . . 13 |- ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } -> y e. RR )
38	37	adantl 482	. . . . . . . . . . . 12 |- ( ( A C_ RR /\ y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } ) -> y e. RR )
39		ssel2 3598	. . . . . . . . . . . 12 |- ( ( A C_ RR /\ y e. A ) -> y e. RR )
40		negeq 10273	. . . . . . . . . . . . . . . 16 |- ( w = y -> -u w = -u y )
41	40	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( w = y -> ( -u w e. { x e. RR | -u x e. A } <-> -u y e. { x e. RR | -u x e. A } ) )
42	41	elrab3 3364	. . . . . . . . . . . . . 14 |- ( y e. RR -> ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } <-> -u y e. { x e. RR | -u x e. A } ) )
43		renegcl 10344	. . . . . . . . . . . . . . 15 |- ( y e. RR -> -u y e. RR )
44		negeq 10273	. . . . . . . . . . . . . . . . 17 |- ( x = -u y -> -u x = -u -u y )
45	44	eleq1d 2686	. . . . . . . . . . . . . . . 16 |- ( x = -u y -> ( -u x e. A <-> -u -u y e. A ) )
46	45	elrab3 3364	. . . . . . . . . . . . . . 15 |- ( -u y e. RR -> ( -u y e. { x e. RR | -u x e. A } <-> -u -u y e. A ) )
47	43, 46	syl 17	. . . . . . . . . . . . . 14 |- ( y e. RR -> ( -u y e. { x e. RR | -u x e. A } <-> -u -u y e. A ) )
48		recn 10026	. . . . . . . . . . . . . . . 16 |- ( y e. RR -> y e. CC )
49	48	negnegd 10383	. . . . . . . . . . . . . . 15 |- ( y e. RR -> -u -u y = y )
50	49	eleq1d 2686	. . . . . . . . . . . . . 14 |- ( y e. RR -> ( -u -u y e. A <-> y e. A ) )
51	42, 47, 50	3bitrd 294	. . . . . . . . . . . . 13 |- ( y e. RR -> ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } <-> y e. A ) )
52	51	adantl 482	. . . . . . . . . . . 12 |- ( ( A C_ RR /\ y e. RR ) -> ( y e. { w e. RR | -u w e. { x e. RR | -u x e. A } } <-> y e. A ) )
53	38, 39, 52	eqrdav 2621	. . . . . . . . . . 11 |- ( A C_ RR -> { w e. RR | -u w e. { x e. RR | -u x e. A } } = A )
54	53	supeq1d 8352	. . . . . . . . . 10 |- ( A C_ RR -> sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) = sup ( A , RR , < ) )
55	54	3ad2ant1 1082	. . . . . . . . 9 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) = sup ( A , RR , < ) )
56	55	negeqd 10275	. . . . . . . 8 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> -u sup ( { w e. RR | -u w e. { x e. RR | -u x e. A } } , RR , < ) = -u sup ( A , RR , < ) )
57	36, 56	eqtrd 2656	. . . . . . 7 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) )
58		infrecl 11005	. . . . . . . . . . 11 |- ( ( { x e. RR | -u x e. A } C_ RR /\ { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
59	32, 58	mp3an1 1411	. . . . . . . . . 10 |- ( ( { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
60	30, 31, 59	syl2an 494	. . . . . . . . 9 |- ( ( ( A C_ RR /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
61	60	3impa 1259	. . . . . . . 8 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
62		suprcl 10983	. . . . . . . 8 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) e. RR )
63		recn 10026	. . . . . . . . 9 |- (inf ( { x e. RR | -u x e. A } , RR , < ) e. RR -> inf ( { x e. RR | -u x e. A } , RR , < ) e. CC )
64		recn 10026	. . . . . . . . 9 |- ( sup ( A , RR , < ) e. RR -> sup ( A , RR , < ) e. CC )
65		negcon2 10334	. . . . . . . . 9 |- ( (inf ( { x e. RR | -u x e. A } , RR , < ) e. CC /\ sup ( A , RR , < ) e. CC ) -> (inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -uinf ( { x e. RR | -u x e. A } , RR , < ) ) )
66	63, 64, 65	syl2an 494	. . . . . . . 8 |- ( (inf ( { x e. RR | -u x e. A } , RR , < ) e. RR /\ sup ( A , RR , < ) e. RR ) -> (inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -uinf ( { x e. RR | -u x e. A } , RR , < ) ) )
67	61, 62, 66	syl2anc 693	. . . . . . 7 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> (inf ( { x e. RR | -u x e. A } , RR , < ) = -u sup ( A , RR , < ) <-> sup ( A , RR , < ) = -uinf ( { x e. RR | -u x e. A } , RR , < ) ) )
68	57, 67	mpbid 222	. . . . . 6 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) = -uinf ( { x e. RR | -u x e. A } , RR , < ) )
69	27, 28, 29, 68	syl3anc 1326	. . . . 5 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) = -uinf ( { x e. RR | -u x e. A } , RR , < ) )
70		supxrre 12157	. . . . . 6 |- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )
71	27, 28, 29, 70	syl3anc 1326	. . . . 5 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )
72	32	a1i 11	. . . . . . . 8 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> { x e. RR | -u x e. A } C_ RR )
73	27, 28, 30	syl2anc 693	. . . . . . . 8 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> { x e. RR | -u x e. A } =/= (/) )
74	29, 31	syl 17	. . . . . . . 8 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z )
75		infxrre 12166	. . . . . . . 8 |- ( ( { x e. RR | -u x e. A } C_ RR /\ { x e. RR | -u x e. A } =/= (/) /\ E. y e. RR A. z e. { x e. RR | -u x e. A } y <_ z ) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = inf ( { x e. RR | -u x e. A } , RR , < ) )
76	72, 73, 74, 75	syl3anc 1326	. . . . . . 7 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = inf ( { x e. RR | -u x e. A } , RR , < ) )
77	76	xnegeqd 39664	. . . . . 6 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -einf ( { x e. RR | -u x e. A } , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR , < ) )
78	26, 60	sylanl1 682	. . . . . . 7 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> inf ( { x e. RR | -u x e. A } , RR , < ) e. RR )
79	78	rexnegd 39334	. . . . . 6 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -einf ( { x e. RR | -u x e. A } , RR , < ) = -uinf ( { x e. RR | -u x e. A } , RR , < ) )
80	77, 79	eqtrd 2656	. . . . 5 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -einf ( { x e. RR | -u x e. A } , RR* , < ) = -uinf ( { x e. RR | -u x e. A } , RR , < ) )
81	69, 71, 80	3eqtr4d 2666	. . . 4 |- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
82		simpr 477	. . . . . . 7 |- ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> -. E. y e. RR A. z e. A z <_ y )
83		simplr 792	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. RR ) /\ z e. A ) -> y e. RR )
84	26	sselda 3603	. . . . . . . . . . . . . 14 |- ( ( ph /\ z e. A ) -> z e. RR )
85	84	adantlr 751	. . . . . . . . . . . . 13 |- ( ( ( ph /\ y e. RR ) /\ z e. A ) -> z e. RR )
86	83, 85	ltnled 10184	. . . . . . . . . . . 12 |- ( ( ( ph /\ y e. RR ) /\ z e. A ) -> ( y < z <-> -. z <_ y ) )
87	86	rexbidva 3049	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( E. z e. A y < z <-> E. z e. A -. z <_ y ) )
88		rexnal 2995	. . . . . . . . . . . 12 |- ( E. z e. A -. z <_ y <-> -. A. z e. A z <_ y )
89	88	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( E. z e. A -. z <_ y <-> -. A. z e. A z <_ y ) )
90	87, 89	bitrd 268	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( E. z e. A y < z <-> -. A. z e. A z <_ y ) )
91	90	ralbidva 2985	. . . . . . . . 9 |- ( ph -> ( A. y e. RR E. z e. A y < z <-> A. y e. RR -. A. z e. A z <_ y ) )
92		ralnex 2992	. . . . . . . . . 10 |- ( A. y e. RR -. A. z e. A z <_ y <-> -. E. y e. RR A. z e. A z <_ y )
93	92	a1i 11	. . . . . . . . 9 |- ( ph -> ( A. y e. RR -. A. z e. A z <_ y <-> -. E. y e. RR A. z e. A z <_ y ) )
94	91, 93	bitrd 268	. . . . . . . 8 |- ( ph -> ( A. y e. RR E. z e. A y < z <-> -. E. y e. RR A. z e. A z <_ y ) )
95	94	adantr 481	. . . . . . 7 |- ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> ( A. y e. RR E. z e. A y < z <-> -. E. y e. RR A. z e. A z <_ y ) )
96	82, 95	mpbird 247	. . . . . 6 |- ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> A. y e. RR E. z e. A y < z )
97		xnegmnf 12041	. . . . . . . . 9 |- -e -oo = +oo
98	97	eqcomi 2631	. . . . . . . 8 |- +oo = -e -oo
99	98	a1i 11	. . . . . . 7 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> +oo = -e -oo )
100		simpr 477	. . . . . . . 8 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> A. y e. RR E. z e. A y < z )
101		ressxr 10083	. . . . . . . . . . . 12 |- RR C_ RR*
102	101	a1i 11	. . . . . . . . . . 11 |- ( ph -> RR C_ RR* )
103	26, 102	sstrd 3613	. . . . . . . . . 10 |- ( ph -> A C_ RR* )
104		supxrunb2 12150	. . . . . . . . . 10 |- ( A C_ RR* -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
105	103, 104	syl 17	. . . . . . . . 9 |- ( ph -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
106	105	adantr 481	. . . . . . . 8 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
107	100, 106	mpbid 222	. . . . . . 7 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> sup ( A , RR* , < ) = +oo )
108		renegcl 10344	. . . . . . . . . . . . . 14 |- ( v e. RR -> -u v e. RR )
109	108	adantl 482	. . . . . . . . . . . . 13 |- ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> -u v e. RR )
110		simpl 473	. . . . . . . . . . . . 13 |- ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> A. y e. RR E. z e. A y < z )
111		breq1 4656	. . . . . . . . . . . . . . 15 |- ( y = -u v -> ( y < z <-> -u v < z ) )
112	111	rexbidv 3052	. . . . . . . . . . . . . 14 |- ( y = -u v -> ( E. z e. A y < z <-> E. z e. A -u v < z ) )
113	112	rspcva 3307	. . . . . . . . . . . . 13 |- ( ( -u v e. RR /\ A. y e. RR E. z e. A y < z ) -> E. z e. A -u v < z )
114	109, 110, 113	syl2anc 693	. . . . . . . . . . . 12 |- ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> E. z e. A -u v < z )
115	114	adantll 750	. . . . . . . . . . 11 |- ( ( ( ph /\ A. y e. RR E. z e. A y < z ) /\ v e. RR ) -> E. z e. A -u v < z )
116		negeq 10273	. . . . . . . . . . . . . . . 16 |- ( x = -u z -> -u x = -u -u z )
117	116	eleq1d 2686	. . . . . . . . . . . . . . 15 |- ( x = -u z -> ( -u x e. A <-> -u -u z e. A ) )
118	84	renegcld 10457	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. A ) -> -u z e. RR )
119	118	ad4ant13 1292	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z e. RR )
120	84	recnd 10068	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ z e. A ) -> z e. CC )
121	120	negnegd 10383	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. A ) -> -u -u z = z )
122		simpr 477	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ z e. A ) -> z e. A )
123	121, 122	eqeltrd 2701	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ z e. A ) -> -u -u z e. A )
124	123	ad4ant13 1292	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u -u z e. A )
125	117, 119, 124	elrabd 3365	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z e. { x e. RR | -u x e. A } )
126		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u v < z )
127	108	ad3antlr 767	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u v e. RR )
128	84	ad4ant13 1292	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> z e. RR )
129	127, 128	ltnegd 10605	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> ( -u v < z <-> -u z < -u -u v ) )
130	126, 129	mpbid 222	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z < -u -u v )
131		simpllr 799	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> v e. RR )
132		recn 10026	. . . . . . . . . . . . . . . 16 |- ( v e. RR -> v e. CC )
133		negneg 10331	. . . . . . . . . . . . . . . 16 |- ( v e. CC -> -u -u v = v )
134	131, 132, 133	3syl 18	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u -u v = v )
135	130, 134	breqtrd 4679	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z < v )
136		breq1 4656	. . . . . . . . . . . . . . 15 |- ( w = -u z -> ( w < v <-> -u z < v ) )
137	136	rspcev 3309	. . . . . . . . . . . . . 14 |- ( ( -u z e. { x e. RR | -u x e. A } /\ -u z < v ) -> E. w e. { x e. RR | -u x e. A } w < v )
138	125, 135, 137	syl2anc 693	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> E. w e. { x e. RR | -u x e. A } w < v )
139	138	rexlimdva2 39339	. . . . . . . . . . . 12 |- ( ( ph /\ v e. RR ) -> ( E. z e. A -u v < z -> E. w e. { x e. RR | -u x e. A } w < v ) )
140	139	adantlr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ A. y e. RR E. z e. A y < z ) /\ v e. RR ) -> ( E. z e. A -u v < z -> E. w e. { x e. RR | -u x e. A } w < v ) )
141	115, 140	mpd 15	. . . . . . . . . 10 |- ( ( ( ph /\ A. y e. RR E. z e. A y < z ) /\ v e. RR ) -> E. w e. { x e. RR | -u x e. A } w < v )
142	141	ralrimiva 2966	. . . . . . . . 9 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> A. v e. RR E. w e. { x e. RR | -u x e. A } w < v )
143	32, 101	sstri 3612	. . . . . . . . . 10 |- { x e. RR | -u x e. A } C_ RR*
144		infxrunb2 39584	. . . . . . . . . 10 |- ( { x e. RR | -u x e. A } C_ RR* -> ( A. v e. RR E. w e. { x e. RR | -u x e. A } w < v <-> inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo ) )
145	143, 144	ax-mp 5	. . . . . . . . 9 |- ( A. v e. RR E. w e. { x e. RR | -u x e. A } w < v <-> inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
146	142, 145	sylib 208	. . . . . . . 8 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> inf ( { x e. RR | -u x e. A } , RR* , < ) = -oo )
147	146	xnegeqd 39664	. . . . . . 7 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> -einf ( { x e. RR | -u x e. A } , RR* , < ) = -e -oo )
148	99, 107, 147	3eqtr4d 2666	. . . . . 6 |- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
149	96, 148	syldan 487	. . . . 5 |- ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
150	149	adantlr 751	. . . 4 |- ( ( ( ph /\ A =/= (/) ) /\ -. E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
151	81, 150	pm2.61dan 832	. . 3 |- ( ( ph /\ A =/= (/) ) -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
152	25, 151	sylan2 491	. 2 |- ( ( ph /\ -. A = (/) ) -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )
153	24, 152	pm2.61dan 832	1 |- ( ph -> sup ( A , RR* , < ) = -einf ( { x e. RR | -u x e. A } , RR* , < ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   C_ wss 3574   (/)c0 3915   class class class wbr 4653   supcsup 8346  infcinf 8347   CCcc 9934   RRcr 9935   +oocpnf 10071   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   -ucneg 10267   -ecxne 11943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-xneg 11946

This theorem is referenced by:  supminfxr2  39699