Metamath Proof Explorer


Theorem supxrrernmpt

Description: The real and extended real indexed suprema match when the indexed real supremum exists. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supxrrernmpt.x 𝑥 𝜑
supxrrernmpt.a ( 𝜑𝐴 ≠ ∅ )
supxrrernmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
supxrrernmpt.y ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑦 )
Assertion supxrrernmpt ( 𝜑 → sup ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑥𝐴𝐵 ) , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 supxrrernmpt.x 𝑥 𝜑
2 supxrrernmpt.a ( 𝜑𝐴 ≠ ∅ )
3 supxrrernmpt.b ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
4 supxrrernmpt.y ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑦 )
5 eqid ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐵 )
6 1 5 3 rnmptssd ( 𝜑 → ran ( 𝑥𝐴𝐵 ) ⊆ ℝ )
7 1 3 5 2 rnmptn0 ( 𝜑 → ran ( 𝑥𝐴𝐵 ) ≠ ∅ )
8 1 4 rnmptbdd ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑧𝑦 )
9 supxrre ( ( ran ( 𝑥𝐴𝐵 ) ⊆ ℝ ∧ ran ( 𝑥𝐴𝐵 ) ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ ran ( 𝑥𝐴𝐵 ) 𝑧𝑦 ) → sup ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑥𝐴𝐵 ) , ℝ , < ) )
10 6 7 8 9 syl3anc ( 𝜑 → sup ( ran ( 𝑥𝐴𝐵 ) , ℝ* , < ) = sup ( ran ( 𝑥𝐴𝐵 ) , ℝ , < ) )