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

Metamath Proof Explorer

Theorem suprubrnmpt2

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

Ref Expression
Hypotheses suprubrnmpt2.x ⊢ Ⅎ x φ
suprubrnmpt2.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
suprubrnmpt2.l ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
suprubrnmpt2.c ⊢ φ → C ∈ A
suprubrnmpt2.d ⊢ φ → D ∈ ℝ
suprubrnmpt2.i ⊢ x = C → B = D
Assertion suprubrnmpt2 ⊢ φ → D ≤ sup ran ⁡ x ∈ A ⟼ B ℝ <

Proof

Step Hyp Ref Expression
1 suprubrnmpt2.x ⊢ Ⅎ x φ
2 suprubrnmpt2.b ⊢ φ ∧ x ∈ A → B ∈ ℝ
3 suprubrnmpt2.l ⊢ φ → ∃ y ∈ ℝ ∀ x ∈ A B ≤ y
4 suprubrnmpt2.c ⊢ φ → C ∈ A
5 suprubrnmpt2.d ⊢ φ → D ∈ ℝ
6 suprubrnmpt2.i ⊢ x = C → B = D
7 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
8 1 7 2 rnmptssd ⊢ φ → ran ⁡ x ∈ A ⟼ B ⊆ ℝ
9 7 6 elrnmpt1s ⊢ C ∈ A ∧ D ∈ ℝ → D ∈ ran ⁡ x ∈ A ⟼ B
10 4 5 9 syl2anc ⊢ φ → D ∈ ran ⁡ x ∈ A ⟼ B
11 10 ne0d ⊢ φ → ran ⁡ x ∈ A ⟼ B ≠ ∅
12 1 3 rnmptbdd ⊢ φ → ∃ y ∈ ℝ ∀ w ∈ ran ⁡ x ∈ A ⟼ B w ≤ y
13 8 11 12 10 suprubd ⊢ φ → D ≤ sup ran ⁡ x ∈ A ⟼ B ℝ <