Metamath Proof Explorer

Theorem supxrre3rnmpt

Description: The indexed supremum of a nonempty set of reals, is real if and only if it is bounded-above . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

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