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

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 ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) , ℝ , < ) )