Description: Closure of the indexed supremum of a nonempty bounded set of reals. Range of a function in maps-to notation can be used, to express an indexed supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | suprclrnmpt.x | ⊢ Ⅎ 𝑥 𝜑 | |
| suprclrnmpt.n | ⊢ ( 𝜑 → 𝐴 ≠ ∅ ) | ||
| suprclrnmpt.b | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) | ||
| suprclrnmpt.y | ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) | ||
| Assertion | suprclrnmpt | ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ∈ ℝ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | suprclrnmpt.x | ⊢ Ⅎ 𝑥 𝜑 | |
| 2 | suprclrnmpt.n | ⊢ ( 𝜑 → 𝐴 ≠ ∅ ) | |
| 3 | suprclrnmpt.b | ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) | |
| 4 | suprclrnmpt.y | ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ) | |
| 5 | eqid | ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |
| 6 | 1 5 3 | rnmptssd | ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ ) |
| 7 | 1 3 5 2 | rnmptn0 | ⊢ ( 𝜑 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ) |
| 8 | 1 4 | rnmptbdd | ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) 𝑧 ≤ 𝑦 ) |
| 9 | 6 7 8 | suprcld | ⊢ ( 𝜑 → sup ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) ∈ ℝ ) |