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

Metamath Proof Explorer

Theorem infxrrnmptcl

Description: The infimum of an arbitrary indexed set of extended reals is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses infxrrnmptcl.1 ⊢ Ⅎ x φ
infxrrnmptcl.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ *
Assertion infxrrnmptcl ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ * < ∈ ℝ *

Proof

Step Hyp Ref Expression
1 infxrrnmptcl.1 ⊢ Ⅎ x φ
2 infxrrnmptcl.2 ⊢ φ ∧ x ∈ A → B ∈ ℝ *
3 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
4 1 3 2 rnmptssd ⊢ φ → ran ⁡ x ∈ A ⟼ B ⊆ ℝ *
5 4 infxrcld ⊢ φ → inf ran ⁡ x ∈ A ⟼ B ℝ * < ∈ ℝ *