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	$$⊢Ⅎx\phi$$
	supxrrernmpt.a	$$⊢\phi \to A\ne \varnothing$$
	supxrrernmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	supxrrernmpt.y	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$
Assertion	supxrrernmpt	$$⊢\phi \to sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)$$

Proof

Step	Hyp	Ref	Expression
1		supxrrernmpt.x	$$⊢Ⅎx\phi$$
2		supxrrernmpt.a	$$⊢\phi \to A\ne \varnothing$$
3		supxrrernmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
4		supxrrernmpt.y	$$⊢\phi \to \exists y\in ℝ\forall x\in AB\le y$$
5		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
6	1 5 3	rnmptssd	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\subseteq ℝ$$
7	1 3 5 2	rnmptn0	$$⊢\phi \to \mathrm{ran}\left(x\in A⟼B\right)\ne \varnothing$$
8	1 4	rnmptbdd	$$⊢\phi \to \exists y\in ℝ\forall z\in \mathrm{ran}\left(x\in A⟼B\right)z\le y$$
9		supxrre	$$⊢\left(\mathrm{ran}\left(x\in A⟼B\right)\subseteq ℝ\wedge \mathrm{ran}\left(x\in A⟼B\right)\ne \varnothing \wedge \exists y\in ℝ\forall z\in \mathrm{ran}\left(x\in A⟼B\right)z\le y\right)\to sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)$$
10	6 7 8 9	syl3anc	$$⊢\phi \to sup\left(\mathrm{ran}\left(x\in A⟼B\right),{ℝ}^{*},<\right)=sup\left(\mathrm{ran}\left(x\in A⟼B\right),ℝ,<\right)$$