This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) , ℝ , < ) )