supminfxr

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)

		Ref	Expression
	Hypothesis	supminfxr.1	\|- ( ph -> A C_ RR )
	Assertion	supminfxr	\|- ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		supminfxr.1	\|- ( ph -> A C_ RR )
2		supeq1	\|- ( A = (/) -> sup ( A , RR* , < ) = sup ( (/) , RR* , < ) )
3		xrsup0	\|- sup ( (/) , RR* , < ) = -oo
4	3	a1i	\|- ( A = (/) -> sup ( (/) , RR* , < ) = -oo )
5	2 4	eqtrd	\|- ( A = (/) -> sup ( A , RR* , < ) = -oo )
6	5	adantl	\|- ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) = -oo )
7		eleq2	\|- ( A = (/) -> ( -u x e. A <-> -u x e. (/) ) )
8	7	rabbidv	\|- ( A = (/) -> { x e. RR \| -u x e. A } = { x e. RR \| -u x e. (/) } )
9		noel	\|- -. -u x e. (/)
10	9	a1i	\|- ( x e. RR -> -. -u x e. (/) )
11	10	rgen	\|- A. x e. RR -. -u x e. (/)
12		rabeq0	\|- ( { x e. RR \| -u x e. (/) } = (/) <-> A. x e. RR -. -u x e. (/) )
13	11 12	mpbir	\|- { x e. RR \| -u x e. (/) } = (/)
14	13	a1i	\|- ( A = (/) -> { x e. RR \| -u x e. (/) } = (/) )
15	8 14	eqtrd	\|- ( A = (/) -> { x e. RR \| -u x e. A } = (/) )
16	15	infeq1d	\|- ( A = (/) -> inf ( { x e. RR \| -u x e. A } , RR* , < ) = inf ( (/) , RR* , < ) )
17		xrinf0	\|- inf ( (/) , RR* , < ) = +oo
18	17	a1i	\|- ( A = (/) -> inf ( (/) , RR* , < ) = +oo )
19	16 18	eqtrd	\|- ( A = (/) -> inf ( { x e. RR \| -u x e. A } , RR* , < ) = +oo )
20	19	xnegeqd	\|- ( A = (/) -> -e inf ( { x e. RR \| -u x e. A } , RR* , < ) = -e +oo )
21		xnegpnf	\|- -e +oo = -oo
22	21	a1i	\|- ( A = (/) -> -e +oo = -oo )
23	20 22	eqtrd	\|- ( A = (/) -> -e inf ( { x e. RR \| -u x e. A } , RR* , < ) = -oo )
24	23	adantl	\|- ( ( ph /\ A = (/) ) -> -e inf ( { x e. RR \| -u x e. A } , RR* , < ) = -oo )
25	6 24	eqtr4d	\|- ( ( ph /\ A = (/) ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )
26		neqne	\|- ( -. A = (/) -> A =/= (/) )
27	1	ad2antrr	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> A C_ RR )
28		simplr	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> A =/= (/) )
29		simpr	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> E. y e. RR A. z e. A z <_ y )
30		negn0	\|- ( ( A C_ RR /\ A =/= (/) ) -> { x e. RR \| -u x e. A } =/= (/) )
31		ublbneg	\|- ( 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	\|- { x e. RR \| -u x e. A } C_ RR
33		infrenegsup	\|- ( ( { 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	\|- ( ( { 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	\|- ( ( ( 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	\|- ( ( 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	\|- ( y e. { w e. RR \| -u w e. { x e. RR \| -u x e. A } } -> y e. RR )
38	37	adantl	\|- ( ( A C_ RR /\ y e. { w e. RR \| -u w e. { x e. RR \| -u x e. A } } ) -> y e. RR )
39		ssel2	\|- ( ( A C_ RR /\ y e. A ) -> y e. RR )
40		negeq	\|- ( w = y -> -u w = -u y )
41	40	eleq1d	\|- ( 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	\|- ( 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	\|- ( y e. RR -> -u y e. RR )
44		negeq	\|- ( x = -u y -> -u x = -u -u y )
45	44	eleq1d	\|- ( x = -u y -> ( -u x e. A <-> -u -u y e. A ) )
46	45	elrab3	\|- ( -u y e. RR -> ( -u y e. { x e. RR \| -u x e. A } <-> -u -u y e. A ) )
47	43 46	syl	\|- ( y e. RR -> ( -u y e. { x e. RR \| -u x e. A } <-> -u -u y e. A ) )
48		recn	\|- ( y e. RR -> y e. CC )
49	48	negnegd	\|- ( y e. RR -> -u -u y = y )
50	49	eleq1d	\|- ( y e. RR -> ( -u -u y e. A <-> y e. A ) )
51	42 47 50	3bitrd	\|- ( y e. RR -> ( y e. { w e. RR \| -u w e. { x e. RR \| -u x e. A } } <-> y e. A ) )
52	51	adantl	\|- ( ( 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	\|- ( A C_ RR -> { w e. RR \| -u w e. { x e. RR \| -u x e. A } } = A )
54	53	supeq1d	\|- ( A C_ RR -> sup ( { w e. RR \| -u w e. { x e. RR \| -u x e. A } } , RR , < ) = sup ( A , RR , < ) )
55	54	3ad2ant1	\|- ( ( 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	\|- ( ( 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	\|- ( ( 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	\|- ( ( { 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	\|- ( ( { 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	\|- ( ( ( 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	\|- ( ( 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	\|- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) e. RR )
63		recn	\|- ( inf ( { x e. RR \| -u x e. A } , RR , < ) e. RR -> inf ( { x e. RR \| -u x e. A } , RR , < ) e. CC )
64		recn	\|- ( sup ( A , RR , < ) e. RR -> sup ( A , RR , < ) e. CC )
65		negcon2	\|- ( ( 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 , < ) = -u inf ( { x e. RR \| -u x e. A } , RR , < ) ) )
66	63 64 65	syl2an	\|- ( ( 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 , < ) = -u inf ( { x e. RR \| -u x e. A } , RR , < ) ) )
67	61 62 66	syl2anc	\|- ( ( 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 , < ) = -u inf ( { x e. RR \| -u x e. A } , RR , < ) ) )
68	57 67	mpbid	\|- ( ( A C_ RR /\ A =/= (/) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) = -u inf ( { x e. RR \| -u x e. A } , RR , < ) )
69	27 28 29 68	syl3anc	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR , < ) = -u inf ( { x e. RR \| -u x e. A } , RR , < ) )
70		supxrre	\|- ( ( 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	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = sup ( A , RR , < ) )
72	32	a1i	\|- ( ( ( 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	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> { x e. RR \| -u x e. A } =/= (/) )
74	29 31	syl	\|- ( ( ( 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	\|- ( ( { 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	\|- ( ( ( 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	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -e inf ( { x e. RR \| -u x e. A } , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR , < ) )
78	1 60	sylanl1	\|- ( ( ( 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	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -e inf ( { x e. RR \| -u x e. A } , RR , < ) = -u inf ( { x e. RR \| -u x e. A } , RR , < ) )
80	77 79	eqtrd	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> -e inf ( { x e. RR \| -u x e. A } , RR* , < ) = -u inf ( { x e. RR \| -u x e. A } , RR , < ) )
81	69 71 80	3eqtr4d	\|- ( ( ( ph /\ A =/= (/) ) /\ E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )
82		simpr	\|- ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> -. E. y e. RR A. z e. A z <_ y )
83		simplr	\|- ( ( ( ph /\ y e. RR ) /\ z e. A ) -> y e. RR )
84	1	sselda	\|- ( ( ph /\ z e. A ) -> z e. RR )
85	84	adantlr	\|- ( ( ( ph /\ y e. RR ) /\ z e. A ) -> z e. RR )
86	83 85	ltnled	\|- ( ( ( ph /\ y e. RR ) /\ z e. A ) -> ( y < z <-> -. z <_ y ) )
87	86	rexbidva	\|- ( ( ph /\ y e. RR ) -> ( E. z e. A y < z <-> E. z e. A -. z <_ y ) )
88		rexnal	\|- ( E. z e. A -. z <_ y <-> -. A. z e. A z <_ y )
89	88	a1i	\|- ( ( ph /\ y e. RR ) -> ( E. z e. A -. z <_ y <-> -. A. z e. A z <_ y ) )
90	87 89	bitrd	\|- ( ( ph /\ y e. RR ) -> ( E. z e. A y < z <-> -. A. z e. A z <_ y ) )
91	90	ralbidva	\|- ( ph -> ( A. y e. RR E. z e. A y < z <-> A. y e. RR -. A. z e. A z <_ y ) )
92		ralnex	\|- ( A. y e. RR -. A. z e. A z <_ y <-> -. E. y e. RR A. z e. A z <_ y )
93	92	a1i	\|- ( 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	\|- ( ph -> ( A. y e. RR E. z e. A y < z <-> -. E. y e. RR A. z e. A z <_ y ) )
95	94	adantr	\|- ( ( 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	\|- ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> A. y e. RR E. z e. A y < z )
97		xnegmnf	\|- -e -oo = +oo
98	97	eqcomi	\|- +oo = -e -oo
99	98	a1i	\|- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> +oo = -e -oo )
100		simpr	\|- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> A. y e. RR E. z e. A y < z )
101		ressxr	\|- RR C_ RR*
102	101	a1i	\|- ( ph -> RR C_ RR* )
103	1 102	sstrd	\|- ( ph -> A C_ RR* )
104		supxrunb2	\|- ( A C_ RR* -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
105	103 104	syl	\|- ( ph -> ( A. y e. RR E. z e. A y < z <-> sup ( A , RR* , < ) = +oo ) )
106	105	adantr	\|- ( ( 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	\|- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> sup ( A , RR* , < ) = +oo )
108		renegcl	\|- ( v e. RR -> -u v e. RR )
109	108	adantl	\|- ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> -u v e. RR )
110		simpl	\|- ( ( 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	\|- ( y = -u v -> ( y < z <-> -u v < z ) )
112	111	rexbidv	\|- ( y = -u v -> ( E. z e. A y < z <-> E. z e. A -u v < z ) )
113	112	rspcva	\|- ( ( -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	\|- ( ( A. y e. RR E. z e. A y < z /\ v e. RR ) -> E. z e. A -u v < z )
115	114	adantll	\|- ( ( ( ph /\ A. y e. RR E. z e. A y < z ) /\ v e. RR ) -> E. z e. A -u v < z )
116		negeq	\|- ( x = -u z -> -u x = -u -u z )
117	116	eleq1d	\|- ( x = -u z -> ( -u x e. A <-> -u -u z e. A ) )
118	84	renegcld	\|- ( ( ph /\ z e. A ) -> -u z e. RR )
119	118	ad4ant13	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z e. RR )
120	84	recnd	\|- ( ( ph /\ z e. A ) -> z e. CC )
121	120	negnegd	\|- ( ( ph /\ z e. A ) -> -u -u z = z )
122		simpr	\|- ( ( ph /\ z e. A ) -> z e. A )
123	121 122	eqeltrd	\|- ( ( ph /\ z e. A ) -> -u -u z e. A )
124	123	ad4ant13	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u -u z e. A )
125	117 119 124	elrabd	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z e. { x e. RR \| -u x e. A } )
126		simpr	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u v < z )
127	108	ad3antlr	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u v e. RR )
128	84	ad4ant13	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> z e. RR )
129	127 128	ltnegd	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> ( -u v < z <-> -u z < -u -u v ) )
130	126 129	mpbid	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z < -u -u v )
131		simpllr	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> v e. RR )
132		recn	\|- ( v e. RR -> v e. CC )
133		negneg	\|- ( v e. CC -> -u -u v = v )
134	131 132 133	3syl	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u -u v = v )
135	130 134	breqtrd	\|- ( ( ( ( ph /\ v e. RR ) /\ z e. A ) /\ -u v < z ) -> -u z < v )
136		breq1	\|- ( w = -u z -> ( w < v <-> -u z < v ) )
137	136	rspcev	\|- ( ( -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	\|- ( ( ( ( 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	\|- ( ( 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	\|- ( ( ( 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	\|- ( ( ( 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	\|- ( ( 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	\|- { x e. RR \| -u x e. A } C_ RR*
144		infxrunb2	\|- ( { 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	\|- ( 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	\|- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> inf ( { x e. RR \| -u x e. A } , RR* , < ) = -oo )
147	146	xnegeqd	\|- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> -e inf ( { x e. RR \| -u x e. A } , RR* , < ) = -e -oo )
148	99 107 147	3eqtr4d	\|- ( ( ph /\ A. y e. RR E. z e. A y < z ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )
149	96 148	syldan	\|- ( ( ph /\ -. E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )
150	149	adantlr	\|- ( ( ( ph /\ A =/= (/) ) /\ -. E. y e. RR A. z e. A z <_ y ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )
151	81 150	pm2.61dan	\|- ( ( ph /\ A =/= (/) ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )
152	26 151	sylan2	\|- ( ( ph /\ -. A = (/) ) -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )
153	25 152	pm2.61dan	\|- ( ph -> sup ( A , RR* , < ) = -e inf ( { x e. RR \| -u x e. A } , RR* , < ) )

Metamath Proof Explorer

Theorem supminfxr

Proof