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 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) → sup ( 𝐴 , ℝ , < ) = - inf ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) )

Proof

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