Theorem supminfrnmpt

Description: The indexed supremum of a bounded-above 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	supminfrnmpt.x	⊢ Ⅎ 𝑥 𝜑
	supminfrnmpt.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
	supminfrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	supminfrnmpt.y	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
Assertion	supminfrnmpt	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - inf ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		supminfrnmpt.x	⊢ Ⅎ 𝑥 𝜑
2		supminfrnmpt.a	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3		supminfrnmpt.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4		supminfrnmpt.y	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6	1 5 3	rnmptssd	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
7	1 3 5 2	rnmptn0	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ )
8	1 4	rnmptbdd	⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 )
9		supminf	⊢ ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - inf ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) )
10	6 7 8 9	syl3anc	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - inf ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) )
11		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ - 𝐵 )
12		simpr	⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
13		renegcl	⊢ ( 𝑤 ∈ ℝ → - 𝑤 ∈ ℝ )
14	5	elrnmpt	⊢ ( - 𝑤 ∈ ℝ → ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 ) )
15	13 14	syl	⊢ ( 𝑤 ∈ ℝ → ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 ) )
16	15	adantr	⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 ) )
17	12 16	mpbid	⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
18	17	adantll	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 )
19		nfv	⊢ Ⅎ 𝑥 𝑤 ∈ ℝ
20	1 19	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ∈ ℝ )
21		negeq	⊢ ( - 𝑤 = 𝐵 → - - 𝑤 = - 𝐵 )
22	21	eqcomd	⊢ ( - 𝑤 = 𝐵 → - 𝐵 = - - 𝑤 )
23	22	adantl	⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑤 = 𝐵 ) → - 𝐵 = - - 𝑤 )
24		recn	⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℂ )
25	24	negnegd	⊢ ( 𝑤 ∈ ℝ → - - 𝑤 = 𝑤 )
26	25	adantr	⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑤 = 𝐵 ) → - - 𝑤 = 𝑤 )
27	23 26	eqtr2d	⊢ ( ( 𝑤 ∈ ℝ ∧ - 𝑤 = 𝐵 ) → 𝑤 = - 𝐵 )
28	27	ex	⊢ ( 𝑤 ∈ ℝ → ( - 𝑤 = 𝐵 → 𝑤 = - 𝐵 ) )
29	28	adantl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( - 𝑤 = 𝐵 → 𝑤 = - 𝐵 ) )
30	29	adantr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝑤 = 𝐵 → 𝑤 = - 𝐵 ) )
31		negeq	⊢ ( 𝑤 = - 𝐵 → - 𝑤 = - - 𝐵 )
32	31	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑤 = - 𝐵 ) → - 𝑤 = - - 𝐵 )
33	3	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
34	33	negnegd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - - 𝐵 = 𝐵 )
35	34	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑤 = - 𝐵 ) → - - 𝐵 = 𝐵 )
36	32 35	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑤 = - 𝐵 ) → - 𝑤 = 𝐵 )
37	36	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 = - 𝐵 → - 𝑤 = 𝐵 ) )
38	37	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑤 = - 𝐵 → - 𝑤 = 𝐵 ) )
39	30 38	impbid	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ) → ( - 𝑤 = 𝐵 ↔ 𝑤 = - 𝐵 ) )
40	20 39	rexbida	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 ) )
41	40	adantr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐴 - 𝑤 = 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 ) )
42	18 41	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑤 = - 𝐵 )
43		simplr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑤 ∈ ℝ )
44	11 42 43	elrnmptd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) → 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
45	44	ex	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
46	45	ralrimiva	⊢ ( 𝜑 → ∀ 𝑤 ∈ ℝ ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
47		rabss	⊢ ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ↔ ∀ 𝑤 ∈ ℝ ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ) )
48	46 47	sylibr	⊢ ( 𝜑 → { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } ⊆ ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
49		nfcv	⊢ Ⅎ 𝑥 - 𝑤
50		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
51	50	nfrn	⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
52	49 51	nfel	⊢ Ⅎ 𝑥 - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
53		nfcv	⊢ Ⅎ 𝑥 ℝ
54	52 53	nfrabw	⊢ Ⅎ 𝑥 { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) }
55	31	eleq1d	⊢ ( 𝑤 = - 𝐵 → ( - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ - - 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) )
56	3	renegcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℝ )
57		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
58	5	elrnmpt1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
59	57 3 58	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
60	34 59	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - - 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
61	55 56 60	elrabd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
62	1 54 11 61	rnmptssdf	⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ⊆ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } )
63	48 62	eqssd	⊢ ( 𝜑 → { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } = ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
64	63	infeq1d	⊢ ( 𝜑 → inf ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) = inf ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
65	64	negeqd	⊢ ( 𝜑 → - inf ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) } , ℝ , < ) = - inf ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )
66	10 65	eqtrd	⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) = - inf ( ran ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )