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