Metamath Proof Explorer

Theorem supminfxr2

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

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

Proof

Step Hyp Ref Expression
1 supminfxr2.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
2 xnegmnf ⊢ -𝑒 -∞ = +∞
3 2 eqcomi ⊢ +∞ = -𝑒 -∞
4 3 a1i ⊢ ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → +∞ = -𝑒 -∞ )
5 supxrpnf ⊢ ( ( 𝐴 ⊆ ℝ* ∧ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
6 1 5 sylan ⊢ ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = +∞ )
7 ssrab2 ⊢ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ⊆ ℝ*
8 7 a1i ⊢ ( +∞ ∈ 𝐴 → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ⊆ ℝ* )
9 xnegeq ⊢ ( 𝑦 = -∞ → -𝑒 𝑦 = -𝑒 -∞ )
10 2 a1i ⊢ ( 𝑦 = -∞ → -𝑒 -∞ = +∞ )
11 9 10 eqtrd ⊢ ( 𝑦 = -∞ → -𝑒 𝑦 = +∞ )
12 11 eleq1d ⊢ ( 𝑦 = -∞ → ( -𝑒 𝑦 ∈ 𝐴 ↔ +∞ ∈ 𝐴 ) )
13 mnfxr ⊢ -∞ ∈ ℝ*
14 13 a1i ⊢ ( +∞ ∈ 𝐴 → -∞ ∈ ℝ* )
15 id ⊢ ( +∞ ∈ 𝐴 → +∞ ∈ 𝐴 )
16 12 14 15 elrabd ⊢ ( +∞ ∈ 𝐴 → -∞ ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } )
17 infxrmnf ⊢ ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ⊆ ℝ* ∧ -∞ ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ) → inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -∞ )
18 8 16 17 syl2anc ⊢ ( +∞ ∈ 𝐴 → inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -∞ )
19 18 adantl ⊢ ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -∞ )
20 19 xnegeqd ⊢ ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -𝑒 -∞ )
21 4 6 20 3eqtr4d ⊢ ( ( 𝜑 ∧ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) )
22 1 ssdifssd ⊢ ( 𝜑 → ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* )
23 22 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → ( 𝐴 ∖ { -∞ } ) ⊆ ℝ* )
24 difssd ⊢ ( ¬ +∞ ∈ 𝐴 → ( 𝐴 ∖ { -∞ } ) ⊆ 𝐴 )
25 id ⊢ ( ¬ +∞ ∈ 𝐴 → ¬ +∞ ∈ 𝐴 )
26 ssnel ⊢ ( ( ( 𝐴 ∖ { -∞ } ) ⊆ 𝐴 ∧ ¬ +∞ ∈ 𝐴 ) → ¬ +∞ ∈ ( 𝐴 ∖ { -∞ } ) )
27 24 25 26 syl2anc ⊢ ( ¬ +∞ ∈ 𝐴 → ¬ +∞ ∈ ( 𝐴 ∖ { -∞ } ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → ¬ +∞ ∈ ( 𝐴 ∖ { -∞ } ) )
29 neldifsnd ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → ¬ -∞ ∈ ( 𝐴 ∖ { -∞ } ) )
30 23 28 29 xrssre ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → ( 𝐴 ∖ { -∞ } ) ⊆ ℝ )
31 30 supminfxr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → sup ( ( 𝐴 ∖ { -∞ } ) , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } , ℝ* , < ) )
32 supxrmnf2 ⊢ ( 𝐴 ⊆ ℝ* → sup ( ( 𝐴 ∖ { -∞ } ) , ℝ* , < ) = sup ( 𝐴 , ℝ* , < ) )
33 1 32 syl ⊢ ( 𝜑 → sup ( ( 𝐴 ∖ { -∞ } ) , ℝ* , < ) = sup ( 𝐴 , ℝ* , < ) )
34 33 eqcomd ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = sup ( ( 𝐴 ∖ { -∞ } ) , ℝ* , < ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = sup ( ( 𝐴 ∖ { -∞ } ) , ℝ* , < ) )
36 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
37 36 adantr ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → 𝑦 ∈ ℝ* )
38 simpl ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → 𝑦 ∈ ℝ )
39 38 rexnegd ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → -𝑒 𝑦 = - 𝑦 )
40 eldifi ⊢ ( - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) → - 𝑦 ∈ 𝐴 )
41 40 adantl ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → - 𝑦 ∈ 𝐴 )
42 39 41 eqeltrd ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → -𝑒 𝑦 ∈ 𝐴 )
43 37 42 jca ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 ∈ 𝐴 ) )
44 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ↔ ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 ∈ 𝐴 ) )
45 43 44 sylibr ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → 𝑦 ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } )
46 renepnf ⊢ ( 𝑦 ∈ ℝ → 𝑦 ≠ +∞ )
47 elsni ⊢ ( 𝑦 ∈ { +∞ } → 𝑦 = +∞ )
48 47 necon3ai ⊢ ( 𝑦 ≠ +∞ → ¬ 𝑦 ∈ { +∞ } )
49 46 48 syl ⊢ ( 𝑦 ∈ ℝ → ¬ 𝑦 ∈ { +∞ } )
50 38 49 syl ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → ¬ 𝑦 ∈ { +∞ } )
51 45 50 eldifd ⊢ ( ( 𝑦 ∈ ℝ ∧ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) → 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) )
52 51 ex ⊢ ( 𝑦 ∈ ℝ → ( - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) → 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) )
53 52 rgen ⊢ ∀ 𝑦 ∈ ℝ ( - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) → 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) )
54 53 a1i ⊢ ( ¬ +∞ ∈ 𝐴 → ∀ 𝑦 ∈ ℝ ( - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) → 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) )
55 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 }
56 nfcv ⊢ Ⅎ 𝑦 { +∞ }
57 55 56 nfdif ⊢ Ⅎ 𝑦 ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } )
58 57 rabssf ⊢ ( { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } ⊆ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ↔ ∀ 𝑦 ∈ ℝ ( - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) → 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) )
59 54 58 sylibr ⊢ ( ¬ +∞ ∈ 𝐴 → { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } ⊆ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) )
60 nfv ⊢ Ⅎ 𝑦 ¬ +∞ ∈ 𝐴
61 nfcv ⊢ Ⅎ 𝑦 ℝ
62 eldifi ⊢ ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) → 𝑦 ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } )
63 7 62 sselid ⊢ ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) → 𝑦 ∈ ℝ* )
64 63 adantl ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → 𝑦 ∈ ℝ* )
65 44 simprbi ⊢ ( 𝑦 ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } → -𝑒 𝑦 ∈ 𝐴 )
66 62 65 syl ⊢ ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) → -𝑒 𝑦 ∈ 𝐴 )
67 12 biimpac ⊢ ( ( -𝑒 𝑦 ∈ 𝐴 ∧ 𝑦 = -∞ ) → +∞ ∈ 𝐴 )
68 67 adantll ⊢ ( ( ( ¬ +∞ ∈ 𝐴 ∧ -𝑒 𝑦 ∈ 𝐴 ) ∧ 𝑦 = -∞ ) → +∞ ∈ 𝐴 )
69 simpll ⊢ ( ( ( ¬ +∞ ∈ 𝐴 ∧ -𝑒 𝑦 ∈ 𝐴 ) ∧ 𝑦 = -∞ ) → ¬ +∞ ∈ 𝐴 )
70 68 69 pm2.65da ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ -𝑒 𝑦 ∈ 𝐴 ) → ¬ 𝑦 = -∞ )
71 70 neqned ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ -𝑒 𝑦 ∈ 𝐴 ) → 𝑦 ≠ -∞ )
72 66 71 sylan2 ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → 𝑦 ≠ -∞ )
73 eldifsni ⊢ ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) → 𝑦 ≠ +∞ )
74 73 adantl ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → 𝑦 ≠ +∞ )
75 64 72 74 xrred ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → 𝑦 ∈ ℝ )
76 60 57 61 75 ssdf2 ⊢ ( ¬ +∞ ∈ 𝐴 → ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ⊆ ℝ )
77 75 rexnegd ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → -𝑒 𝑦 = - 𝑦 )
78 66 adantl ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → -𝑒 𝑦 ∈ 𝐴 )
79 63 adantr ⊢ ( ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ∧ -𝑒 𝑦 ∈ { -∞ } ) → 𝑦 ∈ ℝ* )
80 elsni ⊢ ( -𝑒 𝑦 ∈ { -∞ } → -𝑒 𝑦 = -∞ )
81 80 adantl ⊢ ( ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ∧ -𝑒 𝑦 ∈ { -∞ } ) → -𝑒 𝑦 = -∞ )
82 xnegeq ⊢ ( -𝑒 𝑦 = -∞ → -𝑒 -𝑒 𝑦 = -𝑒 -∞ )
83 2 a1i ⊢ ( -𝑒 𝑦 = -∞ → -𝑒 -∞ = +∞ )
84 82 83 eqtr2d ⊢ ( -𝑒 𝑦 = -∞ → +∞ = -𝑒 -𝑒 𝑦 )
85 84 adantl ⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = -∞ ) → +∞ = -𝑒 -𝑒 𝑦 )
86 xnegneg ⊢ ( 𝑦 ∈ ℝ* → -𝑒 -𝑒 𝑦 = 𝑦 )
87 86 adantr ⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = -∞ ) → -𝑒 -𝑒 𝑦 = 𝑦 )
88 85 87 eqtr2d ⊢ ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = -∞ ) → 𝑦 = +∞ )
89 79 81 88 syl2anc ⊢ ( ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ∧ -𝑒 𝑦 ∈ { -∞ } ) → 𝑦 = +∞ )
90 73 neneqd ⊢ ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) → ¬ 𝑦 = +∞ )
91 90 adantr ⊢ ( ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ∧ -𝑒 𝑦 ∈ { -∞ } ) → ¬ 𝑦 = +∞ )
92 89 91 pm2.65da ⊢ ( 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) → ¬ -𝑒 𝑦 ∈ { -∞ } )
93 92 adantl ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → ¬ -𝑒 𝑦 ∈ { -∞ } )
94 78 93 eldifd ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → -𝑒 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) )
95 77 94 eqeltrrd ⊢ ( ( ¬ +∞ ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ) → - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) )
96 95 ralrimiva ⊢ ( ¬ +∞ ∈ 𝐴 → ∀ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) )
97 76 96 jca ⊢ ( ¬ +∞ ∈ 𝐴 → ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ⊆ ℝ ∧ ∀ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) )
98 57 61 ssrabf ⊢ ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ⊆ { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } ↔ ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ⊆ ℝ ∧ ∀ 𝑦 ∈ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) ) )
99 97 98 sylibr ⊢ ( ¬ +∞ ∈ 𝐴 → ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) ⊆ { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } )
100 59 99 eqssd ⊢ ( ¬ +∞ ∈ 𝐴 → { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } = ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) )
101 100 infeq1d ⊢ ( ¬ +∞ ∈ 𝐴 → inf ( { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } , ℝ* , < ) = inf ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) , ℝ* , < ) )
102 infxrpnf2 ⊢ ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ⊆ ℝ* → inf ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) , ℝ* , < ) = inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) )
103 7 102 ax-mp ⊢ inf ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) , ℝ* , < ) = inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < )
104 103 a1i ⊢ ( ¬ +∞ ∈ 𝐴 → inf ( ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } ∖ { +∞ } ) , ℝ* , < ) = inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) )
105 101 104 eqtr2d ⊢ ( ¬ +∞ ∈ 𝐴 → inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = inf ( { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } , ℝ* , < ) )
106 105 xnegeqd ⊢ ( ¬ +∞ ∈ 𝐴 → -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } , ℝ* , < ) )
107 106 adantl ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ ∣ - 𝑦 ∈ ( 𝐴 ∖ { -∞ } ) } , ℝ* , < ) )
108 31 35 107 3eqtr4d ⊢ ( ( 𝜑 ∧ ¬ +∞ ∈ 𝐴 ) → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) )
109 21 108 pm2.61dan ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) )
110 xnegeq ⊢ ( 𝑦 = 𝑥 → -𝑒 𝑦 = -𝑒 𝑥 )
111 110 eleq1d ⊢ ( 𝑦 = 𝑥 → ( -𝑒 𝑦 ∈ 𝐴 ↔ -𝑒 𝑥 ∈ 𝐴 ) )
112 111 cbvrabv ⊢ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } = { 𝑥 ∈ ℝ* ∣ -𝑒 𝑥 ∈ 𝐴 }
113 112 infeq1i ⊢ inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = inf ( { 𝑥 ∈ ℝ* ∣ -𝑒 𝑥 ∈ 𝐴 } , ℝ* , < )
114 113 xnegeqi ⊢ -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ* ∣ -𝑒 𝑥 ∈ 𝐴 } , ℝ* , < )
115 114 a1i ⊢ ( 𝜑 → -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ 𝐴 } , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ* ∣ -𝑒 𝑥 ∈ 𝐴 } , ℝ* , < ) )
116 109 115 eqtrd ⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = -𝑒 inf ( { 𝑥 ∈ ℝ* ∣ -𝑒 𝑥 ∈ 𝐴 } , ℝ* , < ) )