Metamath Proof Explorer

Theorem supminfrnmpt

Description: The indexed supremum of a bounded-above 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 supminfrnmpt.x ⊢Ⅎxφ
supminfrnmpt.a ⊢φ→A≠∅
supminfrnmpt.b ⊢φ∧x∈A→B∈ℝ
supminfrnmpt.y ⊢φ→∃y∈ℝ∀x∈AB≤y
Assertion supminfrnmpt ⊢φ→supran⁡x∈A⟼Bℝ<=−supran⁡x∈A⟼−Bℝ<

Proof

Step Hyp Ref Expression
1 supminfrnmpt.x ⊢Ⅎxφ
2 supminfrnmpt.a ⊢φ→A≠∅
3 supminfrnmpt.b ⊢φ∧x∈A→B∈ℝ
4 supminfrnmpt.y ⊢φ→∃y∈ℝ∀x∈AB≤y
5 eqid ⊢x∈A⟼B=x∈A⟼B
6 1 5 3 rnmptssd ⊢φ→ran⁡x∈A⟼B⊆ℝ
7 1 3 5 2 rnmptn0 ⊢φ→ran⁡x∈A⟼B≠∅
8 1 4 rnmptbdd ⊢φ→∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤y
9 supminf ⊢ran⁡x∈A⟼B⊆ℝ∧ran⁡x∈A⟼B≠∅∧∃y∈ℝ∀z∈ran⁡x∈A⟼Bz≤y→supran⁡x∈A⟼Bℝ<=−supw∈ℝ|−w∈ran⁡x∈A⟼Bℝ<
10 6 7 8 9 syl3anc ⊢φ→supran⁡x∈A⟼Bℝ<=−supw∈ℝ|−w∈ran⁡x∈A⟼Bℝ<
11 eqid ⊢x∈A⟼−B=x∈A⟼−B
12 simpr ⊢w∈ℝ∧−w∈ran⁡x∈A⟼B→−w∈ran⁡x∈A⟼B
13 renegcl ⊢w∈ℝ→−w∈ℝ
14 5 elrnmpt ⊢−w∈ℝ→−w∈ran⁡x∈A⟼B↔∃x∈A−w=B
15 13 14 syl ⊢w∈ℝ→−w∈ran⁡x∈A⟼B↔∃x∈A−w=B
16 15 adantr ⊢w∈ℝ∧−w∈ran⁡x∈A⟼B→−w∈ran⁡x∈A⟼B↔∃x∈A−w=B
17 12 16 mpbid ⊢w∈ℝ∧−w∈ran⁡x∈A⟼B→∃x∈A−w=B
18 17 adantll ⊢φ∧w∈ℝ∧−w∈ran⁡x∈A⟼B→∃x∈A−w=B
19 nfv ⊢Ⅎxw∈ℝ
20 1 19 nfan ⊢Ⅎxφ∧w∈ℝ
21 negeq ⊢−w=B→−−w=−B
22 21 eqcomd ⊢−w=B→−B=−−w
23 22 adantl ⊢w∈ℝ∧−w=B→−B=−−w
24 recn ⊢w∈ℝ→w∈ℂ
25 24 negnegd ⊢w∈ℝ→−−w=w
26 25 adantr ⊢w∈ℝ∧−w=B→−−w=w
27 23 26 eqtr2d ⊢w∈ℝ∧−w=B→w=−B
28 27 ex ⊢w∈ℝ→−w=B→w=−B
29 28 adantl ⊢φ∧w∈ℝ→−w=B→w=−B
30 29 adantr ⊢φ∧w∈ℝ∧x∈A→−w=B→w=−B
31 negeq ⊢w=−B→−w=−−B
32 31 adantl ⊢φ∧x∈A∧w=−B→−w=−−B
33 3 recnd ⊢φ∧x∈A→B∈ℂ
34 33 negnegd ⊢φ∧x∈A→−−B=B
35 34 adantr ⊢φ∧x∈A∧w=−B→−−B=B
36 32 35 eqtrd ⊢φ∧x∈A∧w=−B→−w=B
37 36 ex ⊢φ∧x∈A→w=−B→−w=B
38 37 adantlr ⊢φ∧w∈ℝ∧x∈A→w=−B→−w=B
39 30 38 impbid ⊢φ∧w∈ℝ∧x∈A→−w=B↔w=−B
40 20 39 rexbida ⊢φ∧w∈ℝ→∃x∈A−w=B↔∃x∈Aw=−B
41 40 adantr ⊢φ∧w∈ℝ∧−w∈ran⁡x∈A⟼B→∃x∈A−w=B↔∃x∈Aw=−B
42 18 41 mpbid ⊢φ∧w∈ℝ∧−w∈ran⁡x∈A⟼B→∃x∈Aw=−B
43 simplr ⊢φ∧w∈ℝ∧−w∈ran⁡x∈A⟼B→w∈ℝ
44 11 42 43 elrnmptd ⊢φ∧w∈ℝ∧−w∈ran⁡x∈A⟼B→w∈ran⁡x∈A⟼−B
45 44 ex ⊢φ∧w∈ℝ→−w∈ran⁡x∈A⟼B→w∈ran⁡x∈A⟼−B
46 45 ralrimiva ⊢φ→∀w∈ℝ−w∈ran⁡x∈A⟼B→w∈ran⁡x∈A⟼−B
47 rabss ⊢w∈ℝ|−w∈ran⁡x∈A⟼B⊆ran⁡x∈A⟼−B↔∀w∈ℝ−w∈ran⁡x∈A⟼B→w∈ran⁡x∈A⟼−B
48 46 47 sylibr ⊢φ→w∈ℝ|−w∈ran⁡x∈A⟼B⊆ran⁡x∈A⟼−B
49 nfcv ⊢Ⅎ_x−w
50 nfmpt1 ⊢Ⅎ_xx∈A⟼B
51 50 nfrn ⊢Ⅎ_xran⁡x∈A⟼B
52 49 51 nfel ⊢Ⅎx−w∈ran⁡x∈A⟼B
53 nfcv ⊢Ⅎ_xℝ
54 52 53 nfrabw ⊢Ⅎ_xw∈ℝ|−w∈ran⁡x∈A⟼B
55 31 eleq1d ⊢w=−B→−w∈ran⁡x∈A⟼B↔−−B∈ran⁡x∈A⟼B
56 3 renegcld ⊢φ∧x∈A→−B∈ℝ
57 simpr ⊢φ∧x∈A→x∈A
58 5 elrnmpt1 ⊢x∈A∧B∈ℝ→B∈ran⁡x∈A⟼B
59 57 3 58 syl2anc ⊢φ∧x∈A→B∈ran⁡x∈A⟼B
60 34 59 eqeltrd ⊢φ∧x∈A→−−B∈ran⁡x∈A⟼B
61 55 56 60 elrabd ⊢φ∧x∈A→−B∈w∈ℝ|−w∈ran⁡x∈A⟼B
62 1 54 11 61 rnmptssdf ⊢φ→ran⁡x∈A⟼−B⊆w∈ℝ|−w∈ran⁡x∈A⟼B
63 48 62 eqssd ⊢φ→w∈ℝ|−w∈ran⁡x∈A⟼B=ran⁡x∈A⟼−B
64 63 infeq1d ⊢φ→supw∈ℝ|−w∈ran⁡x∈A⟼Bℝ<=supran⁡x∈A⟼−Bℝ<
65 64 negeqd ⊢φ→−supw∈ℝ|−w∈ran⁡x∈A⟼Bℝ<=−supran⁡x∈A⟼−Bℝ<
66 10 65 eqtrd ⊢φ→supran⁡x∈A⟼Bℝ<=−supran⁡x∈A⟼−Bℝ<