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	⊢ Ⅎ 𝑥 𝜑
	supminfxrrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
Assertion	supminfxrrnmpt	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		supminfxrrnmpt.x	⊢ Ⅎ 𝑥 𝜑
2		supminfxrrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	1 3 2	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ* )
5	4	supminfxr2	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ* , < ) )
6		xnegex	⊢ -𝑒 𝑦 ∈ V
7	3	elrnmpt	⊢ ( -𝑒 𝑦 ∈ V → ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) )
8	6 7	ax-mp	⊢ ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 )
9	8	biimpi	⊢ ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 )
10		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 )
11		xnegneg	⊢ ( 𝑦 ∈ ℝ* → -𝑒 -𝑒 𝑦 = 𝑦 )
12	11	eqcomd	⊢ ( 𝑦 ∈ ℝ* → 𝑦 = -𝑒 -𝑒 𝑦 )
13	12	adantr	⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → 𝑦 = -𝑒 -𝑒 𝑦 )
14		xnegeq	⊢ ( -𝑒 𝑦 = 𝐵 → -𝑒 -𝑒 𝑦 = -𝑒 𝐵 )
15	14	adantl	⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → -𝑒 -𝑒 𝑦 = -𝑒 𝐵 )
16	13 15	eqtrd	⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → 𝑦 = -𝑒 𝐵 )
17	16	ex	⊢ ( 𝑦 ∈ ℝ* → ( -𝑒 𝑦 = 𝐵 → 𝑦 = -𝑒 𝐵 ) )
18	17	reximdv	⊢ ( 𝑦 ∈ ℝ* → ( ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑦 = -𝑒 𝐵 ) )
19	18	imp	⊢ ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = -𝑒 𝐵 )
20		simpl	⊢ ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ℝ* )
21	10 19 20	elrnmptd	⊢ ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥 ∈ 𝐴 -𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
22	9 21	sylan2	⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
23	22	ex	⊢ ( 𝑦 ∈ ℝ* → ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )
24	23	rgen	⊢ ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
25		rabss	⊢ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ↔ ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) )
26	25	biimpri	⊢ ( ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ) → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
27	24 26	ax-mp	⊢ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 )
28	27	a1i	⊢ ( 𝜑 → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
29		nfcv	⊢ Ⅎ 𝑥 -𝑒 𝑦
30		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
31	30	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
32	29 31	nfel	⊢ Ⅎ 𝑥 -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
33		nfcv	⊢ Ⅎ 𝑥 ℝ*
34	32 33	nfrabw	⊢ Ⅎ 𝑥 { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) }
35		xnegeq	⊢ ( 𝑦 = -𝑒 𝐵 → -𝑒 𝑦 = -𝑒 -𝑒 𝐵 )
36	35	eleq1d	⊢ ( 𝑦 = -𝑒 𝐵 → ( -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ -𝑒 -𝑒 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
37	2	xnegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 𝐵 ∈ ℝ* )
38		xnegneg	⊢ ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 )
39	2 38	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 -𝑒 𝐵 = 𝐵 )
40		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
41	3 40 2	elrnmpt1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
42	39 41	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 -𝑒 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
43	36 37 42	elrabd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → -𝑒 𝐵 ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
44	1 34 10 43	rnmptssdf	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) ⊆ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
45	28 44	eqssd	⊢ ( 𝜑 → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) )
46	45	infeq1d	⊢ ( 𝜑 → inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ* , < ) = inf ( ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )
47	46	xnegeqd	⊢ ( 𝜑 → -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )
48	5 47	eqtrd	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥 ∈ 𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )