Metamath Proof Explorer


Theorem infrenegsup

Description: The infimum of a set of reals A is the negative of the supremum of the negatives of its elements. The antecedent ensures that A is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005) (Revised by AV, 4-Sep-2020)

Ref Expression
Assertion infrenegsup ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 infrecl ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ )
2 1 recnd ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℂ )
3 2 negnegd ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → - - inf ( 𝐴 , ℝ , < ) = inf ( 𝐴 , ℝ , < ) )
4 negeq ( 𝑤 = 𝑧 → - 𝑤 = - 𝑧 )
5 4 cbvmptv ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑧 ∈ ℝ ↦ - 𝑧 )
6 5 mptpreima ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) = { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 }
7 eqid ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 )
8 7 negiso ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) ∧ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) )
9 8 simpri ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 )
10 9 imaeq1i ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 )
11 6 10 eqtr3i { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 )
12 11 supeq1i sup ( { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } , ℝ , < ) = sup ( ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) , ℝ , < )
13 8 simpli ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ )
14 isocnv ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) → ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) )
15 13 14 ax-mp ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ )
16 isoeq1 ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) ) )
17 9 16 ax-mp ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) )
18 15 17 mpbi ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ )
19 18 a1i ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , < ( ℝ , ℝ ) )
20 simp1 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → 𝐴 ⊆ ℝ )
21 infm3 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
22 vex 𝑥 ∈ V
23 vex 𝑦 ∈ V
24 22 23 brcnv ( 𝑥 < 𝑦𝑦 < 𝑥 )
25 24 notbii ( ¬ 𝑥 < 𝑦 ↔ ¬ 𝑦 < 𝑥 )
26 25 ralbii ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 )
27 23 22 brcnv ( 𝑦 < 𝑥𝑥 < 𝑦 )
28 vex 𝑧 ∈ V
29 23 28 brcnv ( 𝑦 < 𝑧𝑧 < 𝑦 )
30 29 rexbii ( ∃ 𝑧𝐴 𝑦 < 𝑧 ↔ ∃ 𝑧𝐴 𝑧 < 𝑦 )
31 27 30 imbi12i ( ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) )
32 31 ralbii ( ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) )
33 26 32 anbi12i ( ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ↔ ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
34 33 rexbii ( ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
35 21 34 sylibr ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 < 𝑥 → ∃ 𝑧𝐴 𝑦 < 𝑧 ) ) )
36 gtso < Or ℝ
37 36 a1i ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → < Or ℝ )
38 19 20 35 37 supiso ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → sup ( ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) , ℝ , < ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , < ) ) )
39 12 38 eqtrid ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → sup ( { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } , ℝ , < ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , < ) ) )
40 df-inf inf ( 𝐴 , ℝ , < ) = sup ( 𝐴 , ℝ , < )
41 40 eqcomi sup ( 𝐴 , ℝ , < ) = inf ( 𝐴 , ℝ , < )
42 41 fveq2i ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , < ) ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ inf ( 𝐴 , ℝ , < ) )
43 negeq ( 𝑤 = inf ( 𝐴 , ℝ , < ) → - 𝑤 = - inf ( 𝐴 , ℝ , < ) )
44 negex - inf ( 𝐴 , ℝ , < ) ∈ V
45 43 7 44 fvmpt ( inf ( 𝐴 , ℝ , < ) ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ inf ( 𝐴 , ℝ , < ) ) = - inf ( 𝐴 , ℝ , < ) )
46 42 45 eqtrid ( inf ( 𝐴 , ℝ , < ) ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , < ) ) = - inf ( 𝐴 , ℝ , < ) )
47 1 46 syl ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , < ) ) = - inf ( 𝐴 , ℝ , < ) )
48 39 47 eqtr2d ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → - inf ( 𝐴 , ℝ , < ) = sup ( { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } , ℝ , < ) )
49 48 negeqd ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → - - inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } , ℝ , < ) )
50 3 49 eqtr3d ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑥𝑦 ) → inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } , ℝ , < ) )