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

Metamath Proof Explorer

Theorem suprubrnmpt

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 suprubrnmpt.x ⊢ Ⅎ 𝑥 𝜑
suprubrnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
suprubrnmpt.e ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
Assertion suprubrnmpt ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 suprubrnmpt.x ⊢ Ⅎ 𝑥 𝜑
2 suprubrnmpt.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 suprubrnmpt.e ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
4 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 1 4 2 rnmptssd ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
7 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
8 4 elrnmpt1 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
9 7 2 8 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
10 9 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ )
11 1 3 rnmptbdd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑤 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑤 ≤ 𝑦 )
13 6 10 12 9 suprubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) )