Metamath Proof Explorer

Theorem supminf

Description: The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011) ( Revised by AV, 13-Sep-2020.)

Ref Expression
Assertion supminf ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → sup A ℝ < = − inf z ∈ ℝ | − z ∈ A ℝ <

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ z ∈ ℝ | − z ∈ A ⊆ ℝ
2 negn0 ⊢ A ⊆ ℝ ∧ A ≠ ∅ → z ∈ ℝ | − z ∈ A ≠ ∅
3 ublbneg ⊢ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y
4 infrenegsup ⊢ z ∈ ℝ | − z ∈ A ⊆ ℝ ∧ z ∈ ℝ | − z ∈ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y → inf z ∈ ℝ | − z ∈ A ℝ < = − sup w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ℝ <
5 1 2 3 4 mp3an3an ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → inf z ∈ ℝ | − z ∈ A ℝ < = − sup w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ℝ <
6 5 3impa ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → inf z ∈ ℝ | − z ∈ A ℝ < = − sup w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ℝ <
7 elrabi ⊢ x ∈ w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A → x ∈ ℝ
8 7 adantl ⊢ A ⊆ ℝ ∧ x ∈ w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A → x ∈ ℝ
9 ssel2 ⊢ A ⊆ ℝ ∧ x ∈ A → x ∈ ℝ
10 negeq ⊢ w = x → − w = − x
11 10 eleq1d ⊢ w = x → − w ∈ z ∈ ℝ | − z ∈ A ↔ − x ∈ z ∈ ℝ | − z ∈ A
12 11 elrab3 ⊢ x ∈ ℝ → x ∈ w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ↔ − x ∈ z ∈ ℝ | − z ∈ A
13 renegcl ⊢ x ∈ ℝ → − x ∈ ℝ
14 negeq ⊢ z = − x → − z = − − x
15 14 eleq1d ⊢ z = − x → − z ∈ A ↔ − − x ∈ A
16 15 elrab3 ⊢ − x ∈ ℝ → − x ∈ z ∈ ℝ | − z ∈ A ↔ − − x ∈ A
17 13 16 syl ⊢ x ∈ ℝ → − x ∈ z ∈ ℝ | − z ∈ A ↔ − − x ∈ A
18 recn ⊢ x ∈ ℝ → x ∈ ℂ
19 18 negnegd ⊢ x ∈ ℝ → − − x = x
20 19 eleq1d ⊢ x ∈ ℝ → − − x ∈ A ↔ x ∈ A
21 12 17 20 3bitrd ⊢ x ∈ ℝ → x ∈ w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ↔ x ∈ A
22 21 adantl ⊢ A ⊆ ℝ ∧ x ∈ ℝ → x ∈ w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ↔ x ∈ A
23 8 9 22 eqrdav ⊢ A ⊆ ℝ → w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A = A
24 23 supeq1d ⊢ A ⊆ ℝ → sup w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ℝ < = sup A ℝ <
25 24 3ad2ant1 ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → sup w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ℝ < = sup A ℝ <
26 25 negeqd ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → − sup w ∈ ℝ | − w ∈ z ∈ ℝ | − z ∈ A ℝ < = − sup A ℝ <
27 6 26 eqtrd ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → inf z ∈ ℝ | − z ∈ A ℝ < = − sup A ℝ <
28 infrecl ⊢ z ∈ ℝ | − z ∈ A ⊆ ℝ ∧ z ∈ ℝ | − z ∈ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ z ∈ ℝ | − z ∈ A x ≤ y → inf z ∈ ℝ | − z ∈ A ℝ < ∈ ℝ
29 1 2 3 28 mp3an3an ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → inf z ∈ ℝ | − z ∈ A ℝ < ∈ ℝ
30 29 3impa ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → inf z ∈ ℝ | − z ∈ A ℝ < ∈ ℝ
31 suprcl ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → sup A ℝ < ∈ ℝ
32 recn ⊢ inf z ∈ ℝ | − z ∈ A ℝ < ∈ ℝ → inf z ∈ ℝ | − z ∈ A ℝ < ∈ ℂ
33 recn ⊢ sup A ℝ < ∈ ℝ → sup A ℝ < ∈ ℂ
34 negcon2 ⊢ inf z ∈ ℝ | − z ∈ A ℝ < ∈ ℂ ∧ sup A ℝ < ∈ ℂ → inf z ∈ ℝ | − z ∈ A ℝ < = − sup A ℝ < ↔ sup A ℝ < = − inf z ∈ ℝ | − z ∈ A ℝ <
35 32 33 34 syl2an ⊢ inf z ∈ ℝ | − z ∈ A ℝ < ∈ ℝ ∧ sup A ℝ < ∈ ℝ → inf z ∈ ℝ | − z ∈ A ℝ < = − sup A ℝ < ↔ sup A ℝ < = − inf z ∈ ℝ | − z ∈ A ℝ <
36 30 31 35 syl2anc ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → inf z ∈ ℝ | − z ∈ A ℝ < = − sup A ℝ < ↔ sup A ℝ < = − inf z ∈ ℝ | − z ∈ A ℝ <
37 27 36 mpbid ⊢ A ⊆ ℝ ∧ A ≠ ∅ ∧ ∃ x ∈ ℝ ∀ y ∈ A y ≤ x → sup A ℝ < = − inf z ∈ ℝ | − z ∈ A ℝ <