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

Metamath Proof Explorer

Theorem supxrrernmpt

Description: The real and extended real indexed suprema match when the indexed real supremum exists. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supxrrernmpt.x ⊢ Ⅎ x φ
supxrrernmpt.a ⊢ φ → A ≠ ∅
supxrrernmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
supxrrernmpt.y ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
Assertion supxrrernmpt ⊢ φ → sup ran ⁡ x ∈ A ⟼ B ℝ * < = sup ran ⁡ x ∈ A ⟼ B ℝ <

Proof

Step Hyp Ref Expression
1 supxrrernmpt.x ⊢ Ⅎ x φ
2 supxrrernmpt.a ⊢ φ → A ≠ ∅
3 supxrrernmpt.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
4 supxrrernmpt.y ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
5 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
6 1 5 3 rnmptssd ⊢ φ → ran ⁡ x ∈ A ⟼ B ⊆ ℝ
7 1 3 5 2 rnmptn0 ⊢ φ → ran ⁡ x ∈ A ⟼ B ≠ ∅
8 1 4 rnmptbdd ⊢ φ → ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y
9 supxrre ⊢ ran ⁡ x ∈ A ⟼ B ⊆ ℝ ∧ ran ⁡ x ∈ A ⟼ B ≠ ∅ ∧ ∃ y ∈ ℝ ∀ z ∈ ran ⁡ x ∈ A ⟼ B z ≤ y → sup ran ⁡ x ∈ A ⟼ B ℝ * < = sup ran ⁡ x ∈ A ⟼ B ℝ <
10 6 7 8 9 syl3anc ⊢ φ → sup ran ⁡ x ∈ A ⟼ B ℝ * < = sup ran ⁡ x ∈ A ⟼ B ℝ <