Theorem supminfxrrnmpt

Description: The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	supminfxrrnmpt.x	|- F/ x ph
	supminfxrrnmpt.b	|- ( ( ph /\ x e. A ) -> B e. RR* )
Assertion	supminfxrrnmpt	|- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = -e inf ( ran ( x e. A |-> -e B ) , RR* , < ) )

Proof

Step	Hyp	Ref	Expression
1		supminfxrrnmpt.x	|- F/ x ph
2		supminfxrrnmpt.b	|- ( ( ph /\ x e. A ) -> B e. RR* )
3		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
4	1 3 2	rnmptssd	|- ( ph -> ran ( x e. A |-> B ) C_ RR* )
5	4	supminfxr2	|- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = -e inf ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } , RR* , < ) )
6		xnegex	|- -e y e. _V
7	3	elrnmpt	|- ( -e y e. _V -> ( -e y e. ran ( x e. A |-> B ) <-> E. x e. A -e y = B ) )
8	6 7	ax-mp	|- ( -e y e. ran ( x e. A |-> B ) <-> E. x e. A -e y = B )
9	8	biimpi	|- ( -e y e. ran ( x e. A |-> B ) -> E. x e. A -e y = B )
10		eqid	|- ( x e. A |-> -e B ) = ( x e. A |-> -e B )
11		xnegneg	|- ( y e. RR* -> -e -e y = y )
12	11	eqcomd	|- ( y e. RR* -> y = -e -e y )
13	12	adantr	|- ( ( y e. RR* /\ -e y = B ) -> y = -e -e y )
14		xnegeq	|- ( -e y = B -> -e -e y = -e B )
15	14	adantl	|- ( ( y e. RR* /\ -e y = B ) -> -e -e y = -e B )
16	13 15	eqtrd	|- ( ( y e. RR* /\ -e y = B ) -> y = -e B )
17	16	ex	|- ( y e. RR* -> ( -e y = B -> y = -e B ) )
18	17	reximdv	|- ( y e. RR* -> ( E. x e. A -e y = B -> E. x e. A y = -e B ) )
19	18	imp	|- ( ( y e. RR* /\ E. x e. A -e y = B ) -> E. x e. A y = -e B )
20		simpl	|- ( ( y e. RR* /\ E. x e. A -e y = B ) -> y e. RR* )
21	10 19 20	elrnmptd	|- ( ( y e. RR* /\ E. x e. A -e y = B ) -> y e. ran ( x e. A |-> -e B ) )
22	9 21	sylan2	|- ( ( y e. RR* /\ -e y e. ran ( x e. A |-> B ) ) -> y e. ran ( x e. A |-> -e B ) )
23	22	ex	|- ( y e. RR* -> ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) ) )
24	23	rgen	|- A. y e. RR* ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) )
25		rabss	|- ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B ) <-> A. y e. RR* ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) ) )
26	25	biimpri	|- ( A. y e. RR* ( -e y e. ran ( x e. A |-> B ) -> y e. ran ( x e. A |-> -e B ) ) -> { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B ) )
27	24 26	ax-mp	|- { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B )
28	27	a1i	|- ( ph -> { y e. RR* | -e y e. ran ( x e. A |-> B ) } C_ ran ( x e. A |-> -e B ) )
29		nfcv	|- F/_ x -e y
30		nfmpt1	|- F/_ x ( x e. A |-> B )
31	30	nfrn	|- F/_ x ran ( x e. A |-> B )
32	29 31	nfel	|- F/ x -e y e. ran ( x e. A |-> B )
33		nfcv	|- F/_ x RR*
34	32 33	nfrabw	|- F/_ x { y e. RR* | -e y e. ran ( x e. A |-> B ) }
35		xnegeq	|- ( y = -e B -> -e y = -e -e B )
36	35	eleq1d	|- ( y = -e B -> ( -e y e. ran ( x e. A |-> B ) <-> -e -e B e. ran ( x e. A |-> B ) ) )
37	2	xnegcld	|- ( ( ph /\ x e. A ) -> -e B e. RR* )
38		xnegneg	|- ( B e. RR* -> -e -e B = B )
39	2 38	syl	|- ( ( ph /\ x e. A ) -> -e -e B = B )
40		simpr	|- ( ( ph /\ x e. A ) -> x e. A )
41	3 40 2	elrnmpt1d	|- ( ( ph /\ x e. A ) -> B e. ran ( x e. A |-> B ) )
42	39 41	eqeltrd	|- ( ( ph /\ x e. A ) -> -e -e B e. ran ( x e. A |-> B ) )
43	36 37 42	elrabd	|- ( ( ph /\ x e. A ) -> -e B e. { y e. RR* | -e y e. ran ( x e. A |-> B ) } )
44	1 34 10 43	rnmptssdf	|- ( ph -> ran ( x e. A |-> -e B ) C_ { y e. RR* | -e y e. ran ( x e. A |-> B ) } )
45	28 44	eqssd	|- ( ph -> { y e. RR* | -e y e. ran ( x e. A |-> B ) } = ran ( x e. A |-> -e B ) )
46	45	infeq1d	|- ( ph -> inf ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } , RR* , < ) = inf ( ran ( x e. A |-> -e B ) , RR* , < ) )
47	46	xnegeqd	|- ( ph -> -e inf ( { y e. RR* | -e y e. ran ( x e. A |-> B ) } , RR* , < ) = -e inf ( ran ( x e. A |-> -e B ) , RR* , < ) )
48	5 47	eqtrd	|- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = -e inf ( ran ( x e. A |-> -e B ) , RR* , < ) )