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