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