This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infxrlbrnmpt2

Description: A member of a nonempty indexed set of reals is greater than or equal to the set's lower bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses infxrlbrnmpt2.x ⊢ Ⅎ x φ
infxrlbrnmpt2.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
infxrlbrnmpt2.c ⊢ φ → C ∈ A
infxrlbrnmpt2.d ⊢ φ → D ∈ ℝ *
infxrlbrnmpt2.e ⊢ x = C → B = D
Assertion infxrlbrnmpt2 ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ * < ≤ D

Proof

Step Hyp Ref Expression
1 infxrlbrnmpt2.x ⊢ Ⅎ x φ
2 infxrlbrnmpt2.b ⊢ φ ∧ x ∈ A → B ∈ ℝ *
3 infxrlbrnmpt2.c ⊢ φ → C ∈ A
4 infxrlbrnmpt2.d ⊢ φ → D ∈ ℝ *
5 infxrlbrnmpt2.e ⊢ x = C → B = D
6 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
7 1 6 2 rnmptssd ⊢ φ → ran ⁡ x ∈ A ⟼ B ⊆ ℝ *
8 6 5 elrnmpt1s ⊢ C ∈ A ∧ D ∈ ℝ * → D ∈ ran ⁡ x ∈ A ⟼ B
9 3 4 8 syl2anc ⊢ φ → D ∈ ran ⁡ x ∈ A ⟼ B
10 infxrlb ⊢ ran ⁡ x ∈ A ⟼ B ⊆ ℝ * ∧ D ∈ ran ⁡ x ∈ A ⟼ B → inf ran ⁡ x ∈ A ⟼ B ℝ * < ≤ D
11 7 9 10 syl2anc ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ * < ≤ D