Metamath Proof Explorer

Theorem supminfxr

Description: The extended real suprema of a set of reals is the extended real negative of the extended real infima of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis supminfxr.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
Assertion supminfxr ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 supminfxr.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 supeq1 ⊢ ( 𝐴 = ∅ → sup ( 𝐴 , ℝ* , < ) = sup ( ∅ , ℝ* , < ) )
3 xrsup0 ⊢ sup ( ∅ , ℝ* , < ) = -∞
4 3 a1i ⊢ ( 𝐴 = ∅ → sup ( ∅ , ℝ* , < ) = -∞ )
5 2 4 eqtrd ⊢ ( 𝐴 = ∅ → sup ( 𝐴 , ℝ* , < ) = -∞ )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) = -∞ )
7 eleq2 ⊢ ( 𝐴 = ∅ → ( - 𝑥 ∈ 𝐴 ↔ - 𝑥 ∈ ∅ ) )
8 7 rabbidv ⊢ ( 𝐴 = ∅ → { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } = { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ ∅ } )
9 noel ⊢ ¬ - 𝑥 ∈ ∅
10 9 a1i ⊢ ( 𝑥 ∈ ℝ → ¬ - 𝑥 ∈ ∅ )
11 10 rgen ⊢ ∀ 𝑥 ∈ ℝ ¬ - 𝑥 ∈ ∅
12 rabeq0 ⊢ ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ ∅ } = ∅ ↔ ∀ 𝑥 ∈ ℝ ¬ - 𝑥 ∈ ∅ )
13 11 12 mpbir ⊢ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ ∅ } = ∅
14 13 a1i ⊢ ( 𝐴 = ∅ → { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ ∅ } = ∅ )
15 8 14 eqtrd ⊢ ( 𝐴 = ∅ → { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } = ∅ )
16 15 infeq1d ⊢ ( 𝐴 = ∅ → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = inf ( ∅ , ℝ* , < ) )
17 xrinf0 ⊢ inf ( ∅ , ℝ* , < ) = +∞
18 17 a1i ⊢ ( 𝐴 = ∅ → inf ( ∅ , ℝ* , < ) = +∞ )
19 16 18 eqtrd ⊢ ( 𝐴 = ∅ → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = +∞ )
20 19 xnegeqd ⊢ ( 𝐴 = ∅ → -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -𝑒 +∞ )
21 xnegpnf ⊢ -𝑒 +∞ = -∞
22 21 a1i ⊢ ( 𝐴 = ∅ → -𝑒 +∞ = -∞ )
23 20 22 eqtrd ⊢ ( 𝐴 = ∅ → -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -∞ )
24 23 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -∞ )
25 6 24 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )
26 neqne ⊢ ( ¬ 𝐴 = ∅ → 𝐴 ≠ ∅ )
27 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → 𝐴 ⊆ ℝ )
28 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → 𝐴 ≠ ∅ )
29 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 )
30 negn0 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) → { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ≠ ∅ )
31 ublbneg ⊢ ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑦 ≤ 𝑧 )
32 ssrab2 ⊢ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ⊆ ℝ
33 infrenegsup ⊢ ( ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ⊆ ℝ ∧ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑦 ≤ 𝑧 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } , ℝ , < ) )
34 32 33 mp3an1 ⊢ ( ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑦 ≤ 𝑧 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } , ℝ , < ) )
35 30 31 34 syl2an ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } , ℝ , < ) )
36 35 3impa ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } , ℝ , < ) )
37 elrabi ⊢ ( 𝑦 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } → 𝑦 ∈ ℝ )
38 37 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } ) → 𝑦 ∈ ℝ )
39 ssel2 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
40 negeq ⊢ ( 𝑤 = 𝑦 → - 𝑤 = - 𝑦 )
41 40 eleq1d ⊢ ( 𝑤 = 𝑦 → ( - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ↔ - 𝑦 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ) )
42 41 elrab3 ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } ↔ - 𝑦 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ) )
43 renegcl ⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ )
44 negeq ⊢ ( 𝑥 = - 𝑦 → - 𝑥 = - - 𝑦 )
45 44 eleq1d ⊢ ( 𝑥 = - 𝑦 → ( - 𝑥 ∈ 𝐴 ↔ - - 𝑦 ∈ 𝐴 ) )
46 45 elrab3 ⊢ ( - 𝑦 ∈ ℝ → ( - 𝑦 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ↔ - - 𝑦 ∈ 𝐴 ) )
47 43 46 syl ⊢ ( 𝑦 ∈ ℝ → ( - 𝑦 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ↔ - - 𝑦 ∈ 𝐴 ) )
48 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
49 48 negnegd ⊢ ( 𝑦 ∈ ℝ → - - 𝑦 = 𝑦 )
50 49 eleq1d ⊢ ( 𝑦 ∈ ℝ → ( - - 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
51 42 47 50 3bitrd ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } ↔ 𝑦 ∈ 𝐴 ) )
52 51 adantl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } ↔ 𝑦 ∈ 𝐴 ) )
53 38 39 52 eqrdav ⊢ ( 𝐴 ⊆ ℝ → { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } = 𝐴 )
54 53 supeq1d ⊢ ( 𝐴 ⊆ ℝ → sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } , ℝ , < ) = sup ( 𝐴 , ℝ , < ) )
55 54 3ad2ant1 ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } , ℝ , < ) = sup ( 𝐴 , ℝ , < ) )
56 55 negeqd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → - sup ( { 𝑤 ∈ ℝ ∣ - 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } } , ℝ , < ) = - sup ( 𝐴 , ℝ , < ) )
57 36 56 eqtrd ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( 𝐴 , ℝ , < ) )
58 infrecl ⊢ ( ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ⊆ ℝ ∧ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑦 ≤ 𝑧 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
59 32 58 mp3an1 ⊢ ( ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑦 ≤ 𝑧 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
60 30 31 59 syl2an ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
61 60 3impa ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
62 suprcl ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ , < ) ∈ ℝ )
63 recn ⊢ ( inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℂ )
64 recn ⊢ ( sup ( 𝐴 , ℝ , < ) ∈ ℝ → sup ( 𝐴 , ℝ , < ) ∈ ℂ )
65 negcon2 ⊢ ( ( inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℂ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℂ ) → ( inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( 𝐴 , ℝ , < ) ↔ sup ( 𝐴 , ℝ , < ) = - inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ) )
66 63 64 65 syl2an ⊢ ( ( inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ ∧ sup ( 𝐴 , ℝ , < ) ∈ ℝ ) → ( inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( 𝐴 , ℝ , < ) ↔ sup ( 𝐴 , ℝ , < ) = - inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ) )
67 61 62 66 syl2anc ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → ( inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - sup ( 𝐴 , ℝ , < ) ↔ sup ( 𝐴 , ℝ , < ) = - inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ) )
68 57 67 mpbid ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ , < ) = - inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) )
69 27 28 29 68 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ , < ) = - inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) )
70 supxrre ⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ* , < ) = sup ( 𝐴 , ℝ , < ) )
71 27 28 29 70 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ* , < ) = sup ( 𝐴 , ℝ , < ) )
72 32 a1i ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ⊆ ℝ )
73 27 28 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ≠ ∅ )
74 29 31 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑦 ≤ 𝑧 )
75 infxrre ⊢ ( ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ⊆ ℝ ∧ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑦 ≤ 𝑧 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) )
76 72 73 74 75 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) )
77 76 xnegeqd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) )
78 1 60 sylanl1 ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) ∈ ℝ )
79 78 rexnegd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) = - inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) )
80 77 79 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = - inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ , < ) )
81 69 71 80 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )
82 simpr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 )
83 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
84 1 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
85 84 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ )
86 83 85 ltnled ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑦 ) )
87 86 rexbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ) )
88 rexnal ⊢ ( ∃ 𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 )
89 88 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 ¬ 𝑧 ≤ 𝑦 ↔ ¬ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) )
90 87 89 bitrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) )
91 90 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) )
92 ralnex ⊢ ( ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 )
93 92 a1i ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ¬ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ↔ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) )
94 91 93 bitrd ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) )
95 94 adantr ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) )
96 82 95 mpbird ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
97 xnegmnf ⊢ -𝑒 -∞ = +∞
98 97 eqcomi ⊢ +∞ = -𝑒 -∞
99 98 a1i ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → +∞ = -𝑒 -∞ )
100 simpr ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
101 ressxr ⊢ ℝ ⊆ ℝ*
102 101 a1i ⊢ ( 𝜑 → ℝ ⊆ ℝ* )
103 1 102 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
104 supxrunb2 ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
105 103 104 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
106 105 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ sup ( 𝐴 , ℝ* , < ) = +∞ ) )
107 100 106 mpbid ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
108 renegcl ⊢ ( 𝑣 ∈ ℝ → - 𝑣 ∈ ℝ )
109 108 adantl ⊢ ( ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ ) → - 𝑣 ∈ ℝ )
110 simpl ⊢ ( ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ ) → ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 )
111 breq1 ⊢ ( 𝑦 = - 𝑣 → ( 𝑦 < 𝑧 ↔ - 𝑣 < 𝑧 ) )
112 111 rexbidv ⊢ ( 𝑦 = - 𝑣 → ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 - 𝑣 < 𝑧 ) )
113 112 rspcva ⊢ ( ( - 𝑣 ∈ ℝ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → ∃ 𝑧 ∈ 𝐴 - 𝑣 < 𝑧 )
114 109 110 113 syl2anc ⊢ ( ( ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ∧ 𝑣 ∈ ℝ ) → ∃ 𝑧 ∈ 𝐴 - 𝑣 < 𝑧 )
115 114 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ∧ 𝑣 ∈ ℝ ) → ∃ 𝑧 ∈ 𝐴 - 𝑣 < 𝑧 )
116 negeq ⊢ ( 𝑥 = - 𝑧 → - 𝑥 = - - 𝑧 )
117 116 eleq1d ⊢ ( 𝑥 = - 𝑧 → ( - 𝑥 ∈ 𝐴 ↔ - - 𝑧 ∈ 𝐴 ) )
118 84 renegcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → - 𝑧 ∈ ℝ )
119 118 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - 𝑧 ∈ ℝ )
120 84 recnd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℂ )
121 120 negnegd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → - - 𝑧 = 𝑧 )
122 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
123 121 122 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → - - 𝑧 ∈ 𝐴 )
124 123 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - - 𝑧 ∈ 𝐴 )
125 117 119 124 elrabd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } )
126 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - 𝑣 < 𝑧 )
127 108 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - 𝑣 ∈ ℝ )
128 84 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → 𝑧 ∈ ℝ )
129 127 128 ltnegd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → ( - 𝑣 < 𝑧 ↔ - 𝑧 < - - 𝑣 ) )
130 126 129 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - 𝑧 < - - 𝑣 )
131 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → 𝑣 ∈ ℝ )
132 recn ⊢ ( 𝑣 ∈ ℝ → 𝑣 ∈ ℂ )
133 negneg ⊢ ( 𝑣 ∈ ℂ → - - 𝑣 = 𝑣 )
134 131 132 133 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - - 𝑣 = 𝑣 )
135 130 134 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → - 𝑧 < 𝑣 )
136 breq1 ⊢ ( 𝑤 = - 𝑧 → ( 𝑤 < 𝑣 ↔ - 𝑧 < 𝑣 ) )
137 136 rspcev ⊢ ( ( - 𝑧 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ∧ - 𝑧 < 𝑣 ) → ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 )
138 125 135 137 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) ∧ - 𝑣 < 𝑧 ) → ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 )
139 138 rexlimdva2 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 - 𝑣 < 𝑧 → ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 ) )
140 139 adantlr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ∧ 𝑣 ∈ ℝ ) → ( ∃ 𝑧 ∈ 𝐴 - 𝑣 < 𝑧 → ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 ) )
141 115 140 mpd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ∧ 𝑣 ∈ ℝ ) → ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 )
142 141 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → ∀ 𝑣 ∈ ℝ ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 )
143 32 101 sstri ⊢ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ⊆ ℝ*
144 infxrunb2 ⊢ ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } ⊆ ℝ* → ( ∀ 𝑣 ∈ ℝ ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 ↔ inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -∞ ) )
145 143 144 ax-mp ⊢ ( ∀ 𝑣 ∈ ℝ ∃ 𝑤 ∈ { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } 𝑤 < 𝑣 ↔ inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -∞ )
146 142 145 sylib ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -∞ )
147 146 xnegeqd ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) = -𝑒 -∞ )
148 99 107 147 3eqtr4d ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )
149 96 148 syldan ⊢ ( ( 𝜑 ∧ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )
150 149 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ ¬ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝐴 𝑧 ≤ 𝑦 ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )
151 81 150 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )
152 26 151 sylan2 ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )
153 25 152 pm2.61dan ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ ∣ - 𝑥 ∈ 𝐴 } , ℝ* , < ) )