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 𝑥 𝜑
suprubrnmpt2.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
suprubrnmpt2.l ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑦 )
suprubrnmpt2.c ( 𝜑𝐶𝐴 )
suprubrnmpt2.d ( 𝜑𝐷 ∈ ℝ )
suprubrnmpt2.i ( 𝑥 = 𝐶𝐵 = 𝐷 )
Assertion suprubrnmpt2 ( 𝜑𝐷 ≤ sup ( ran ( 𝑥𝐴𝐵 ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 suprubrnmpt2.x 𝑥 𝜑
2 suprubrnmpt2.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
3 suprubrnmpt2.l ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑦 )
4 suprubrnmpt2.c ( 𝜑𝐶𝐴 )
5 suprubrnmpt2.d ( 𝜑𝐷 ∈ ℝ )
6 suprubrnmpt2.i ( 𝑥 = 𝐶𝐵 = 𝐷 )
7 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
8 1 7 2 rnmptssd ( 𝜑 → ran ( 𝑥𝐴𝐵 ) ⊆ ℝ )
9 7 6 elrnmpt1s ( ( 𝐶𝐴𝐷 ∈ ℝ ) → 𝐷 ∈ ran ( 𝑥𝐴𝐵 ) )
10 4 5 9 syl2anc ( 𝜑𝐷 ∈ ran ( 𝑥𝐴𝐵 ) )
11 10 ne0d ( 𝜑 → ran ( 𝑥𝐴𝐵 ) ≠ ∅ )
12 1 3 rnmptbdd ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥𝐴𝐵 ) 𝑤𝑦 )
13 8 11 12 10 suprubd ( 𝜑𝐷 ≤ sup ( ran ( 𝑥𝐴𝐵 ) , ℝ , < ) )