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 ⊢ Ⅎ x φ
supminfrnmpt.a ⊢ φ → A ≠ ∅
supminfrnmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
supminfrnmpt.y ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
Assertion supminfrnmpt ⊢ φ → sup ran ⁡ x ∈ A ⟼ B ℝ < = − sup ran ⁡ x ∈ A ⟼ − B ℝ <

Proof

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