Metamath Proof Explorer

Theorem supxrleubrnmpt

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

Ref Expression
Hypotheses supxrleubrnmpt.x ⊢Ⅎxφ
supxrleubrnmpt.b ⊢φ∧x∈A→B∈ℝ*
supxrleubrnmpt.c ⊢φ→C∈ℝ*
Assertion supxrleubrnmpt ⊢φ→supran⁡x∈A⟼Bℝ*<≤C↔∀x∈AB≤C

Proof

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