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	|- F/ x ph
	supxrrernmpt.a	|- ( ph -> A =/= (/) )
	supxrrernmpt.b	|- ( ( ph /\ x e. A ) -> B e. RR )
	supxrrernmpt.y	|- ( ph -> E. y e. RR A. x e. A B <_ y )
Assertion	supxrrernmpt	|- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( x e. A |-> B ) , RR , < ) )

Proof

Step	Hyp	Ref	Expression
1		supxrrernmpt.x	|- F/ x ph
2		supxrrernmpt.a	|- ( ph -> A =/= (/) )
3		supxrrernmpt.b	|- ( ( ph /\ x e. A ) -> B e. RR )
4		supxrrernmpt.y	|- ( ph -> E. y e. RR A. x e. A B <_ y )
5		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
6	1 5 3	rnmptssd	|- ( ph -> ran ( x e. A |-> B ) C_ RR )
7	1 3 5 2	rnmptn0	|- ( ph -> ran ( x e. A |-> B ) =/= (/) )
8	1 4	rnmptbdd	|- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
9		supxrre	|- ( ( ran ( x e. A |-> B ) C_ RR /\ ran ( x e. A |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) -> sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( x e. A |-> B ) , RR , < ) )
10	6 7 8 9	syl3anc	|- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( x e. A |-> B ) , RR , < ) )