Metamath Proof Explorer

Theorem suprleubrnmpt

Description: The supremum of a nonempty bounded indexed set of reals is less than or equal to an upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses suprleubrnmpt.x ⊢Ⅎxφ
suprleubrnmpt.a ⊢φ→A≠∅
suprleubrnmpt.b ⊢φ∧x∈A→B∈ℝ
suprleubrnmpt.e ⊢φ→∃y∈ℝ∀x∈AB≤y
suprleubrnmpt.c ⊢φ→C∈ℝ
Assertion suprleubrnmpt ⊢φ→supran⁡x∈A⟼Bℝ<≤C↔∀x∈AB≤C

Proof

Step Hyp Ref Expression
1 suprleubrnmpt.x ⊢Ⅎxφ
2 suprleubrnmpt.a ⊢φ→A≠∅
3 suprleubrnmpt.b ⊢φ∧x∈A→B∈ℝ
4 suprleubrnmpt.e ⊢φ→∃y∈ℝ∀x∈AB≤y
5 suprleubrnmpt.c ⊢φ→C∈ℝ
6 eqid ⊢x∈A⟼B=x∈A⟼B
7 1 6 3 rnmptssd ⊢φ→ran⁡x∈A⟼B⊆ℝ
8 1 3 6 2 rnmptn0 ⊢φ→ran⁡x∈A⟼B≠∅
9 1 4 rnmptbdd ⊢φ→∃y∈ℝ∀w∈ran⁡x∈A⟼Bw≤y
10 suprleub ⊢ran⁡x∈A⟼B⊆ℝ∧ran⁡x∈A⟼B≠∅∧∃y∈ℝ∀w∈ran⁡x∈A⟼Bw≤y∧C∈ℝ→supran⁡x∈A⟼Bℝ<≤C↔∀z∈ran⁡x∈A⟼Bz≤C
11 7 8 9 5 10 syl31anc ⊢φ→supran⁡x∈A⟼Bℝ<≤C↔∀z∈ran⁡x∈A⟼Bz≤C
12 nfmpt1 ⊢Ⅎ_xx∈A⟼B
13 12 nfrn ⊢Ⅎ_xran⁡x∈A⟼B
14 nfv ⊢Ⅎxz≤C
15 13 14 nfralw ⊢Ⅎx∀z∈ran⁡x∈A⟼Bz≤C
16 1 15 nfan ⊢Ⅎxφ∧∀z∈ran⁡x∈A⟼Bz≤C
17 simpr ⊢φ∧x∈A→x∈A
18 6 elrnmpt1 ⊢x∈A∧B∈ℝ→B∈ran⁡x∈A⟼B
19 17 3 18 syl2anc ⊢φ∧x∈A→B∈ran⁡x∈A⟼B
20 19 adantlr ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤C∧x∈A→B∈ran⁡x∈A⟼B
21 simplr ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤C∧x∈A→∀z∈ran⁡x∈A⟼Bz≤C
22 breq1 ⊢z=B→z≤C↔B≤C
23 22 rspcva ⊢B∈ran⁡x∈A⟼B∧∀z∈ran⁡x∈A⟼Bz≤C→B≤C
24 20 21 23 syl2anc ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤C∧x∈A→B≤C
25 24 ex ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤C→x∈A→B≤C
26 16 25 ralrimi ⊢φ∧∀z∈ran⁡x∈A⟼Bz≤C→∀x∈AB≤C
27 26 ex ⊢φ→∀z∈ran⁡x∈A⟼Bz≤C→∀x∈AB≤C
28 vex ⊢z∈V
29 6 elrnmpt ⊢z∈V→z∈ran⁡x∈A⟼B↔∃x∈Az=B
30 28 29 ax-mp ⊢z∈ran⁡x∈A⟼B↔∃x∈Az=B
31 30 biimpi ⊢z∈ran⁡x∈A⟼B→∃x∈Az=B
32 31 adantl ⊢∀x∈AB≤C∧z∈ran⁡x∈A⟼B→∃x∈Az=B
33 nfra1 ⊢Ⅎx∀x∈AB≤C
34 rspa ⊢∀x∈AB≤C∧x∈A→B≤C
35 22 biimprcd ⊢B≤C→z=B→z≤C
36 34 35 syl ⊢∀x∈AB≤C∧x∈A→z=B→z≤C
37 36 ex ⊢∀x∈AB≤C→x∈A→z=B→z≤C
38 33 14 37 rexlimd ⊢∀x∈AB≤C→∃x∈Az=B→z≤C
39 38 adantr ⊢∀x∈AB≤C∧z∈ran⁡x∈A⟼B→∃x∈Az=B→z≤C
40 32 39 mpd ⊢∀x∈AB≤C∧z∈ran⁡x∈A⟼B→z≤C
41 40 ralrimiva ⊢∀x∈AB≤C→∀z∈ran⁡x∈A⟼Bz≤C
42 41 a1i ⊢φ→∀x∈AB≤C→∀z∈ran⁡x∈A⟼Bz≤C
43 27 42 impbid ⊢φ→∀z∈ran⁡x∈A⟼Bz≤C↔∀x∈AB≤C
44 11 43 bitrd ⊢φ→supran⁡x∈A⟼Bℝ<≤C↔∀x∈AB≤C