Metamath Proof Explorer

Theorem infxrgelbrnmpt

Description: The infimum of an indexed set of extended reals is greater than or equal to a lower bound. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step Hyp Ref Expression
1 infxrgelbrnmpt.x ⊢Ⅎxφ
2 infxrgelbrnmpt.b ⊢φ∧x∈A→B∈ℝ*
3 infxrgelbrnmpt.c ⊢φ→C∈ℝ*
4 eqid ⊢x∈A⟼B=x∈A⟼B
5 1 4 2 rnmptssd ⊢φ→ran⁡x∈A⟼B⊆ℝ*
6 infxrgelb ⊢ran⁡x∈A⟼B⊆ℝ*∧C∈ℝ*→C≤supran⁡x∈A⟼Bℝ*<↔∀z∈ran⁡x∈A⟼BC≤z
7 5 3 6 syl2anc ⊢φ→C≤supran⁡x∈A⟼Bℝ*<↔∀z∈ran⁡x∈A⟼BC≤z
8 nfmpt1 ⊢Ⅎ_xx∈A⟼B
9 8 nfrn ⊢Ⅎ_xran⁡x∈A⟼B
10 nfv ⊢ℲxC≤z
11 9 10 nfralw ⊢Ⅎx∀z∈ran⁡x∈A⟼BC≤z
12 1 11 nfan ⊢Ⅎxφ∧∀z∈ran⁡x∈A⟼BC≤z
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⟼BC≤z∧x∈A→B∈ran⁡x∈A⟼B
17 simplr ⊢φ∧∀z∈ran⁡x∈A⟼BC≤z∧x∈A→∀z∈ran⁡x∈A⟼BC≤z
18 breq2 ⊢z=B→C≤z↔C≤B
19 18 rspcva ⊢B∈ran⁡x∈A⟼B∧∀z∈ran⁡x∈A⟼BC≤z→C≤B
20 16 17 19 syl2anc ⊢φ∧∀z∈ran⁡x∈A⟼BC≤z∧x∈A→C≤B
21 20 ex ⊢φ∧∀z∈ran⁡x∈A⟼BC≤z→x∈A→C≤B
22 12 21 ralrimi ⊢φ∧∀z∈ran⁡x∈A⟼BC≤z→∀x∈AC≤B
23 vex ⊢z∈V
24 4 elrnmpt ⊢z∈V→z∈ran⁡x∈A⟼B↔∃x∈Az=B
25 23 24 ax-mp ⊢z∈ran⁡x∈A⟼B↔∃x∈Az=B
26 25 biimpi ⊢z∈ran⁡x∈A⟼B→∃x∈Az=B
27 26 adantl ⊢∀x∈AC≤B∧z∈ran⁡x∈A⟼B→∃x∈Az=B
28 nfra1 ⊢Ⅎx∀x∈AC≤B
29 rspa ⊢∀x∈AC≤B∧x∈A→C≤B
30 18 biimprcd ⊢C≤B→z=B→C≤z
31 29 30 syl ⊢∀x∈AC≤B∧x∈A→z=B→C≤z
32 31 ex ⊢∀x∈AC≤B→x∈A→z=B→C≤z
33 28 10 32 rexlimd ⊢∀x∈AC≤B→∃x∈Az=B→C≤z
34 33 adantr ⊢∀x∈AC≤B∧z∈ran⁡x∈A⟼B→∃x∈Az=B→C≤z
35 27 34 mpd ⊢∀x∈AC≤B∧z∈ran⁡x∈A⟼B→C≤z
36 35 ralrimiva ⊢∀x∈AC≤B→∀z∈ran⁡x∈A⟼BC≤z
37 36 adantl ⊢φ∧∀x∈AC≤B→∀z∈ran⁡x∈A⟼BC≤z
38 22 37 impbida ⊢φ→∀z∈ran⁡x∈A⟼BC≤z↔∀x∈AC≤B
39 7 38 bitrd ⊢φ→C≤supran⁡x∈A⟼Bℝ*<↔∀x∈AC≤B