Metamath Proof Explorer


Theorem supminfxrrnmpt

Description: The indexed supremum of a set of reals is the negation of the indexed infimum of that set's image under negation. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses supminfxrrnmpt.x 𝑥 𝜑
supminfxrrnmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
Assertion supminfxrrnmpt ( 𝜑 → sup ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )

Proof

Step Hyp Ref Expression
1 supminfxrrnmpt.x 𝑥 𝜑
2 supminfxrrnmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ* )
3 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
4 1 3 2 rnmptssd ( 𝜑 → ran ( 𝑥𝐴𝐵 ) ⊆ ℝ* )
5 4 supminfxr2 ( 𝜑 → sup ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) = -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } , ℝ* , < ) )
6 xnegex -𝑒 𝑦 ∈ V
7 3 elrnmpt ( -𝑒 𝑦 ∈ V → ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) ↔ ∃ 𝑥𝐴 -𝑒 𝑦 = 𝐵 ) )
8 6 7 ax-mp ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) ↔ ∃ 𝑥𝐴 -𝑒 𝑦 = 𝐵 )
9 8 biimpi ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) → ∃ 𝑥𝐴 -𝑒 𝑦 = 𝐵 )
10 eqid ( 𝑥𝐴 ↦ -𝑒 𝐵 ) = ( 𝑥𝐴 ↦ -𝑒 𝐵 )
11 xnegneg ( 𝑦 ∈ ℝ* → -𝑒 -𝑒 𝑦 = 𝑦 )
12 11 eqcomd ( 𝑦 ∈ ℝ*𝑦 = -𝑒 -𝑒 𝑦 )
13 12 adantr ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → 𝑦 = -𝑒 -𝑒 𝑦 )
14 xnegeq ( -𝑒 𝑦 = 𝐵 → -𝑒 -𝑒 𝑦 = -𝑒 𝐵 )
15 14 adantl ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → -𝑒 -𝑒 𝑦 = -𝑒 𝐵 )
16 13 15 eqtrd ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 = 𝐵 ) → 𝑦 = -𝑒 𝐵 )
17 16 ex ( 𝑦 ∈ ℝ* → ( -𝑒 𝑦 = 𝐵𝑦 = -𝑒 𝐵 ) )
18 17 reximdv ( 𝑦 ∈ ℝ* → ( ∃ 𝑥𝐴 -𝑒 𝑦 = 𝐵 → ∃ 𝑥𝐴 𝑦 = -𝑒 𝐵 ) )
19 18 imp ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥𝐴 -𝑒 𝑦 = 𝐵 ) → ∃ 𝑥𝐴 𝑦 = -𝑒 𝐵 )
20 simpl ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥𝐴 -𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ℝ* )
21 10 19 20 elrnmptd ( ( 𝑦 ∈ ℝ* ∧ ∃ 𝑥𝐴 -𝑒 𝑦 = 𝐵 ) → 𝑦 ∈ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) )
22 9 21 sylan2 ( ( 𝑦 ∈ ℝ* ∧ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) ) → 𝑦 ∈ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) )
23 22 ex ( 𝑦 ∈ ℝ* → ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) → 𝑦 ∈ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) ) )
24 23 rgen 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) → 𝑦 ∈ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) )
25 rabss ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } ⊆ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) ↔ ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) → 𝑦 ∈ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) ) )
26 25 biimpri ( ∀ 𝑦 ∈ ℝ* ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) → 𝑦 ∈ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) ) → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } ⊆ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) )
27 24 26 ax-mp { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } ⊆ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 )
28 27 a1i ( 𝜑 → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } ⊆ ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) )
29 nfcv 𝑥 -𝑒 𝑦
30 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
31 30 nfrn 𝑥 ran ( 𝑥𝐴𝐵 )
32 29 31 nfel 𝑥 -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 )
33 nfcv 𝑥*
34 32 33 nfrabw 𝑥 { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) }
35 xnegeq ( 𝑦 = -𝑒 𝐵 → -𝑒 𝑦 = -𝑒 -𝑒 𝐵 )
36 35 eleq1d ( 𝑦 = -𝑒 𝐵 → ( -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) ↔ -𝑒 -𝑒 𝐵 ∈ ran ( 𝑥𝐴𝐵 ) ) )
37 2 xnegcld ( ( 𝜑𝑥𝐴 ) → -𝑒 𝐵 ∈ ℝ* )
38 xnegneg ( 𝐵 ∈ ℝ* → -𝑒 -𝑒 𝐵 = 𝐵 )
39 2 38 syl ( ( 𝜑𝑥𝐴 ) → -𝑒 -𝑒 𝐵 = 𝐵 )
40 simpr ( ( 𝜑𝑥𝐴 ) → 𝑥𝐴 )
41 3 40 2 elrnmpt1d ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ran ( 𝑥𝐴𝐵 ) )
42 39 41 eqeltrd ( ( 𝜑𝑥𝐴 ) → -𝑒 -𝑒 𝐵 ∈ ran ( 𝑥𝐴𝐵 ) )
43 36 37 42 elrabd ( ( 𝜑𝑥𝐴 ) → -𝑒 𝐵 ∈ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } )
44 1 34 10 43 rnmptssdf ( 𝜑 → ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) ⊆ { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } )
45 28 44 eqssd ( 𝜑 → { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } = ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) )
46 45 infeq1d ( 𝜑 → inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } , ℝ* , < ) = inf ( ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )
47 46 xnegeqd ( 𝜑 → -𝑒 inf ( { 𝑦 ∈ ℝ* ∣ -𝑒 𝑦 ∈ ran ( 𝑥𝐴𝐵 ) } , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )
48 5 47 eqtrd ( 𝜑 → sup ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) = -𝑒 inf ( ran ( 𝑥𝐴 ↦ -𝑒 𝐵 ) , ℝ* , < ) )