Theorem 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	$$⊢\phi \to A\subseteq ℝ$$
Assertion	supminfxr	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		supminfxr.1	$$⊢\phi \to A\subseteq ℝ$$
2		supeq1	$$⊢A=\varnothing \to sup\left(A,{ℝ}^{*},<\right)=sup\left(\varnothing ,{ℝ}^{*},<\right)$$
3		xrsup0	$$⊢sup\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{-\infty }$$
4	3	a1i	$$⊢A=\varnothing \to sup\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{-\infty }$$
5	2 4	eqtrd	$$⊢A=\varnothing \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }$$
6	5	adantl	$$⊢\left(\phi \wedge A=\varnothing \right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{-\infty }$$
7		eleq2	$$⊢A=\varnothing \to \left(-x\in A\leftrightarrow -x\in \varnothing \right)$$
8	7	rabbidv	$$⊢A=\varnothing \to \left\{x\in ℝ|-x\in A\right\}=\left\{x\in ℝ|-x\in \varnothing \right\}$$
9		noel	$$⊢\neg -x\in \varnothing$$
10	9	a1i	$$⊢x\in ℝ\to \neg -x\in \varnothing$$
11	10	rgen	$$⊢\forall x\in ℝ\neg -x\in \varnothing$$
12		rabeq0	$$⊢\left\{x\in ℝ|-x\in \varnothing \right\}=\varnothing \leftrightarrow \forall x\in ℝ\neg -x\in \varnothing$$
13	11 12	mpbir	$$⊢\left\{x\in ℝ|-x\in \varnothing \right\}=\varnothing$$
14	13	a1i	$$⊢A=\varnothing \to \left\{x\in ℝ|-x\in \varnothing \right\}=\varnothing$$
15	8 14	eqtrd	$$⊢A=\varnothing \to \left\{x\in ℝ|-x\in A\right\}=\varnothing$$
16	15	infeq1d	$$⊢A=\varnothing \to inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=inf\left(\varnothing ,{ℝ}^{*},<\right)$$
17		xrinf0	$$⊢inf\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
18	17	a1i	$$⊢A=\varnothing \to inf\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
19	16 18	eqtrd	$$⊢A=\varnothing \to inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=\mathrm{+\infty }$$
20	19	xnegeqd	$$⊢A=\varnothing \to -inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=-\mathrm{+\infty }$$
21		xnegpnf	$$⊢-\mathrm{+\infty }=\mathrm{-\infty }$$
22	21	a1i	$$⊢A=\varnothing \to -\mathrm{+\infty }=\mathrm{-\infty }$$
23	20 22	eqtrd	$$⊢A=\varnothing \to -inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$$
24	23	adantl	$$⊢\left(\phi \wedge A=\varnothing \right)\to -inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$$
25	6 24	eqtr4d	$$⊢\left(\phi \wedge A=\varnothing \right)\to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$
26		neqne	$$⊢\neg A=\varnothing \to A\ne \varnothing$$
27	1	ad2antrr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to A\subseteq ℝ$$
28		simplr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to A\ne \varnothing$$
29		simpr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to \exists y\in ℝ\forall z\in Az\le y$$
30		negn0	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\to \left\{x\in ℝ|-x\in A\right\}\ne \varnothing$$
31		ublbneg	$$⊢\exists y\in ℝ\forall z\in Az\le y\to \exists y\in ℝ\forall z\in \left\{x\in ℝ|-x\in A\right\}y\le z$$
32		ssrab2	$$⊢\left\{x\in ℝ|-x\in A\right\}\subseteq ℝ$$
33		infrenegsup	$$⊢\left(\left\{x\in ℝ|-x\in A\right\}\subseteq ℝ\wedge \left\{x\in ℝ|-x\in A\right\}\ne \varnothing \wedge \exists y\in ℝ\forall z\in \left\{x\in ℝ|-x\in A\right\}y\le z\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(\left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\},ℝ,<\right)$$
34	32 33	mp3an1	$$⊢\left(\left\{x\in ℝ|-x\in A\right\}\ne \varnothing \wedge \exists y\in ℝ\forall z\in \left\{x\in ℝ|-x\in A\right\}y\le z\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(\left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\},ℝ,<\right)$$
35	30 31 34	syl2an	$$⊢\left(\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(\left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\},ℝ,<\right)$$
36	35	3impa	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(\left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\},ℝ,<\right)$$
37		elrabi	$$⊢y\in \left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\}\to y\in ℝ$$
38	37	adantl	$$⊢\left(A\subseteq ℝ\wedge y\in \left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\}\right)\to y\in ℝ$$
39		ssel2	$$⊢\left(A\subseteq ℝ\wedge y\in A\right)\to y\in ℝ$$
40		negeq	$$⊢w=y\to -w=-y$$
41	40	eleq1d	$$⊢w=y\to \left(-w\in \left\{x\in ℝ|-x\in A\right\}\leftrightarrow -y\in \left\{x\in ℝ|-x\in A\right\}\right)$$
42	41	elrab3	$$⊢y\in ℝ\to \left(y\in \left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\}\leftrightarrow -y\in \left\{x\in ℝ|-x\in A\right\}\right)$$
43		renegcl	$$⊢y\in ℝ\to -y\in ℝ$$
44		negeq	$$⊢x=-y\to -x=-\left(-y\right)$$
45	44	eleq1d	$$⊢x=-y\to \left(-x\in A\leftrightarrow -\left(-y\right)\in A\right)$$
46	45	elrab3	$$⊢-y\in ℝ\to \left(-y\in \left\{x\in ℝ|-x\in A\right\}\leftrightarrow -\left(-y\right)\in A\right)$$
47	43 46	syl	$$⊢y\in ℝ\to \left(-y\in \left\{x\in ℝ|-x\in A\right\}\leftrightarrow -\left(-y\right)\in A\right)$$
48		recn	$$⊢y\in ℝ\to y\in ℂ$$
49	48	negnegd	$$⊢y\in ℝ\to -\left(-y\right)=y$$
50	49	eleq1d	$$⊢y\in ℝ\to \left(-\left(-y\right)\in A\leftrightarrow y\in A\right)$$
51	42 47 50	3bitrd	$$⊢y\in ℝ\to \left(y\in \left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\}\leftrightarrow y\in A\right)$$
52	51	adantl	$$⊢\left(A\subseteq ℝ\wedge y\in ℝ\right)\to \left(y\in \left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\}\leftrightarrow y\in A\right)$$
53	38 39 52	eqrdav	$$⊢A\subseteq ℝ\to \left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\}=A$$
54	53	supeq1d	$$⊢A\subseteq ℝ\to sup\left(\left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\},ℝ,<\right)=sup\left(A,ℝ,<\right)$$
55	54	3ad2ant1	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(\left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\},ℝ,<\right)=sup\left(A,ℝ,<\right)$$
56	55	negeqd	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to -sup\left(\left\{w\in ℝ|-w\in \left\{x\in ℝ|-x\in A\right\}\right\},ℝ,<\right)=-sup\left(A,ℝ,<\right)$$
57	36 56	eqtrd	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(A,ℝ,<\right)$$
58		infrecl	$$⊢\left(\left\{x\in ℝ|-x\in A\right\}\subseteq ℝ\wedge \left\{x\in ℝ|-x\in A\right\}\ne \varnothing \wedge \exists y\in ℝ\forall z\in \left\{x\in ℝ|-x\in A\right\}y\le z\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℝ$$
59	32 58	mp3an1	$$⊢\left(\left\{x\in ℝ|-x\in A\right\}\ne \varnothing \wedge \exists y\in ℝ\forall z\in \left\{x\in ℝ|-x\in A\right\}y\le z\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℝ$$
60	30 31 59	syl2an	$$⊢\left(\left(A\subseteq ℝ\wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℝ$$
61	60	3impa	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℝ$$
62		suprcl	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,ℝ,<\right)\in ℝ$$
63		recn	$$⊢inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℝ\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℂ$$
64		recn	$$⊢sup\left(A,ℝ,<\right)\in ℝ\to sup\left(A,ℝ,<\right)\in ℂ$$
65		negcon2	$$⊢\left(inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℂ\wedge sup\left(A,ℝ,<\right)\in ℂ\right)\to \left(inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(A,ℝ,<\right)\leftrightarrow sup\left(A,ℝ,<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\right)$$
66	63 64 65	syl2an	$$⊢\left(inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℝ\wedge sup\left(A,ℝ,<\right)\in ℝ\right)\to \left(inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(A,ℝ,<\right)\leftrightarrow sup\left(A,ℝ,<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\right)$$
67	61 62 66	syl2anc	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to \left(inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-sup\left(A,ℝ,<\right)\leftrightarrow sup\left(A,ℝ,<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\right)$$
68	57 67	mpbid	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,ℝ,<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)$$
69	27 28 29 68	syl3anc	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,ℝ,<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)$$
70		supxrre	$$⊢\left(A\subseteq ℝ\wedge A\ne \varnothing \wedge \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,{ℝ}^{*},<\right)=sup\left(A,ℝ,<\right)$$
71	27 28 29 70	syl3anc	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,{ℝ}^{*},<\right)=sup\left(A,ℝ,<\right)$$
72	32	a1i	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to \left\{x\in ℝ|-x\in A\right\}\subseteq ℝ$$
73	27 28 30	syl2anc	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to \left\{x\in ℝ|-x\in A\right\}\ne \varnothing$$
74	29 31	syl	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to \exists y\in ℝ\forall z\in \left\{x\in ℝ|-x\in A\right\}y\le z$$
75		infxrre	$$⊢\left(\left\{x\in ℝ|-x\in A\right\}\subseteq ℝ\wedge \left\{x\in ℝ|-x\in A\right\}\ne \varnothing \wedge \exists y\in ℝ\forall z\in \left\{x\in ℝ|-x\in A\right\}y\le z\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)$$
76	72 73 74 75	syl3anc	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)$$
77	76	xnegeqd	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to -inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)$$
78	1 60	sylanl1	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)\in ℝ$$
79	78	rexnegd	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to -inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)$$
80	77 79	eqtrd	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to -inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},ℝ,<\right)$$
81	69 71 80	3eqtr4d	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$
82		simpr	$$⊢\left(\phi \wedge \neg \exists y\in ℝ\forall z\in Az\le y\right)\to \neg \exists y\in ℝ\forall z\in Az\le y$$
83		simplr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge z\in A\right)\to y\in ℝ$$
84	1	sselda	$$⊢\left(\phi \wedge z\in A\right)\to z\in ℝ$$
85	84	adantlr	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge z\in A\right)\to z\in ℝ$$
86	83 85	ltnled	$$⊢\left(\left(\phi \wedge y\in ℝ\right)\wedge z\in A\right)\to \left(y<z\leftrightarrow \neg z\le y\right)$$
87	86	rexbidva	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left(\exists z\in Ay<z\leftrightarrow \exists z\in A\neg z\le y\right)$$
88		rexnal	$$⊢\exists z\in A\neg z\le y\leftrightarrow \neg \forall z\in Az\le y$$
89	88	a1i	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left(\exists z\in A\neg z\le y\leftrightarrow \neg \forall z\in Az\le y\right)$$
90	87 89	bitrd	$$⊢\left(\phi \wedge y\in ℝ\right)\to \left(\exists z\in Ay<z\leftrightarrow \neg \forall z\in Az\le y\right)$$
91	90	ralbidva	$$⊢\phi \to \left(\forall y\in ℝ\exists z\in Ay<z\leftrightarrow \forall y\in ℝ\neg \forall z\in Az\le y\right)$$
92		ralnex	$$⊢\forall y\in ℝ\neg \forall z\in Az\le y\leftrightarrow \neg \exists y\in ℝ\forall z\in Az\le y$$
93	92	a1i	$$⊢\phi \to \left(\forall y\in ℝ\neg \forall z\in Az\le y\leftrightarrow \neg \exists y\in ℝ\forall z\in Az\le y\right)$$
94	91 93	bitrd	$$⊢\phi \to \left(\forall y\in ℝ\exists z\in Ay<z\leftrightarrow \neg \exists y\in ℝ\forall z\in Az\le y\right)$$
95	94	adantr	$$⊢\left(\phi \wedge \neg \exists y\in ℝ\forall z\in Az\le y\right)\to \left(\forall y\in ℝ\exists z\in Ay<z\leftrightarrow \neg \exists y\in ℝ\forall z\in Az\le y\right)$$
96	82 95	mpbird	$$⊢\left(\phi \wedge \neg \exists y\in ℝ\forall z\in Az\le y\right)\to \forall y\in ℝ\exists z\in Ay<z$$
97		xnegmnf	$$⊢-\mathrm{-\infty }=\mathrm{+\infty }$$
98	97	eqcomi	$$⊢\mathrm{+\infty }=-\mathrm{-\infty }$$
99	98	a1i	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to \mathrm{+\infty }=-\mathrm{-\infty }$$
100		simpr	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to \forall y\in ℝ\exists z\in Ay<z$$
101		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
102	101	a1i	$$⊢\phi \to ℝ\subseteq {ℝ}^{*}$$
103	1 102	sstrd	$$⊢\phi \to A\subseteq {ℝ}^{*}$$
104		supxrunb2	$$⊢A\subseteq {ℝ}^{*}\to \left(\forall y\in ℝ\exists z\in Ay<z\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$$
105	103 104	syl	$$⊢\phi \to \left(\forall y\in ℝ\exists z\in Ay<z\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$$
106	105	adantr	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to \left(\forall y\in ℝ\exists z\in Ay<z\leftrightarrow sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }\right)$$
107	100 106	mpbid	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
108		renegcl	$$⊢v\in ℝ\to -v\in ℝ$$
109	108	adantl	$$⊢\left(\forall y\in ℝ\exists z\in Ay<z\wedge v\in ℝ\right)\to -v\in ℝ$$
110		simpl	$$⊢\left(\forall y\in ℝ\exists z\in Ay<z\wedge v\in ℝ\right)\to \forall y\in ℝ\exists z\in Ay<z$$
111		breq1	$$⊢y=-v\to \left(y<z\leftrightarrow -v<z\right)$$
112	111	rexbidv	$$⊢y=-v\to \left(\exists z\in Ay<z\leftrightarrow \exists z\in A-v<z\right)$$
113	112	rspcva	$$⊢\left(-v\in ℝ\wedge \forall y\in ℝ\exists z\in Ay<z\right)\to \exists z\in A-v<z$$
114	109 110 113	syl2anc	$$⊢\left(\forall y\in ℝ\exists z\in Ay<z\wedge v\in ℝ\right)\to \exists z\in A-v<z$$
115	114	adantll	$$⊢\left(\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\wedge v\in ℝ\right)\to \exists z\in A-v<z$$
116		negeq	$$⊢x=-z\to -x=-\left(-z\right)$$
117	116	eleq1d	$$⊢x=-z\to \left(-x\in A\leftrightarrow -\left(-z\right)\in A\right)$$
118	84	renegcld	$$⊢\left(\phi \wedge z\in A\right)\to -z\in ℝ$$
119	118	ad4ant13	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -z\in ℝ$$
120	84	recnd	$$⊢\left(\phi \wedge z\in A\right)\to z\in ℂ$$
121	120	negnegd	$$⊢\left(\phi \wedge z\in A\right)\to -\left(-z\right)=z$$
122		simpr	$$⊢\left(\phi \wedge z\in A\right)\to z\in A$$
123	121 122	eqeltrd	$$⊢\left(\phi \wedge z\in A\right)\to -\left(-z\right)\in A$$
124	123	ad4ant13	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -\left(-z\right)\in A$$
125	117 119 124	elrabd	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -z\in \left\{x\in ℝ|-x\in A\right\}$$
126		simpr	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -v<z$$
127	108	ad3antlr	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -v\in ℝ$$
128	84	ad4ant13	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to z\in ℝ$$
129	127 128	ltnegd	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to \left(-v<z\leftrightarrow -z<-\left(-v\right)\right)$$
130	126 129	mpbid	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -z<-\left(-v\right)$$
131		simpllr	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to v\in ℝ$$
132		recn	$$⊢v\in ℝ\to v\in ℂ$$
133		negneg	$$⊢v\in ℂ\to -\left(-v\right)=v$$
134	131 132 133	3syl	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -\left(-v\right)=v$$
135	130 134	breqtrd	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to -z<v$$
136		breq1	$$⊢w=-z\to \left(w<v\leftrightarrow -z<v\right)$$
137	136	rspcev	$$⊢\left(-z\in \left\{x\in ℝ|-x\in A\right\}\wedge -z<v\right)\to \exists w\in \left\{x\in ℝ|-x\in A\right\}w<v$$
138	125 135 137	syl2anc	$$⊢\left(\left(\left(\phi \wedge v\in ℝ\right)\wedge z\in A\right)\wedge -v<z\right)\to \exists w\in \left\{x\in ℝ|-x\in A\right\}w<v$$
139	138	rexlimdva2	$$⊢\left(\phi \wedge v\in ℝ\right)\to \left(\exists z\in A-v<z\to \exists w\in \left\{x\in ℝ|-x\in A\right\}w<v\right)$$
140	139	adantlr	$$⊢\left(\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\wedge v\in ℝ\right)\to \left(\exists z\in A-v<z\to \exists w\in \left\{x\in ℝ|-x\in A\right\}w<v\right)$$
141	115 140	mpd	$$⊢\left(\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\wedge v\in ℝ\right)\to \exists w\in \left\{x\in ℝ|-x\in A\right\}w<v$$
142	141	ralrimiva	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to \forall v\in ℝ\exists w\in \left\{x\in ℝ|-x\in A\right\}w<v$$
143	32 101	sstri	$$⊢\left\{x\in ℝ|-x\in A\right\}\subseteq {ℝ}^{*}$$
144		infxrunb2	$$⊢\left\{x\in ℝ|-x\in A\right\}\subseteq {ℝ}^{*}\to \left(\forall v\in ℝ\exists w\in \left\{x\in ℝ|-x\in A\right\}w<v\leftrightarrow inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }\right)$$
145	143 144	ax-mp	$$⊢\forall v\in ℝ\exists w\in \left\{x\in ℝ|-x\in A\right\}w<v\leftrightarrow inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$$
146	142 145	sylib	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=\mathrm{-\infty }$$
147	146	xnegeqd	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to -inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)=-\mathrm{-\infty }$$
148	99 107 147	3eqtr4d	$$⊢\left(\phi \wedge \forall y\in ℝ\exists z\in Ay<z\right)\to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$
149	96 148	syldan	$$⊢\left(\phi \wedge \neg \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$
150	149	adantlr	$$⊢\left(\left(\phi \wedge A\ne \varnothing \right)\wedge \neg \exists y\in ℝ\forall z\in Az\le y\right)\to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$
151	81 150	pm2.61dan	$$⊢\left(\phi \wedge A\ne \varnothing \right)\to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$
152	26 151	sylan2	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$
153	25 152	pm2.61dan	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=-inf\left(\left\{x\in ℝ|-x\in A\right\},{ℝ}^{*},<\right)$$