Theorem suprubrnmpt2

Description: A member of a nonempty indexed set of reals is less than or equal to the set's upper bound. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	suprubrnmpt2.x	|- F/ x ph
	suprubrnmpt2.b	|- ( ( ph /\ x e. A ) -> B e. RR )
	suprubrnmpt2.l	|- ( ph -> E. y e. RR A. x e. A B <_ y )
	suprubrnmpt2.c	|- ( ph -> C e. A )
	suprubrnmpt2.d	|- ( ph -> D e. RR )
	suprubrnmpt2.i	|- ( x = C -> B = D )
Assertion	suprubrnmpt2	|- ( ph -> D <_ sup ( ran ( x e. A |-> B ) , RR , < ) )

Proof

Step	Hyp	Ref	Expression
1		suprubrnmpt2.x	|- F/ x ph
2		suprubrnmpt2.b	|- ( ( ph /\ x e. A ) -> B e. RR )
3		suprubrnmpt2.l	|- ( ph -> E. y e. RR A. x e. A B <_ y )
4		suprubrnmpt2.c	|- ( ph -> C e. A )
5		suprubrnmpt2.d	|- ( ph -> D e. RR )
6		suprubrnmpt2.i	|- ( x = C -> B = D )
7		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
8	1 7 2	rnmptssd	|- ( ph -> ran ( x e. A |-> B ) C_ RR )
9	7 6	elrnmpt1s	|- ( ( C e. A /\ D e. RR ) -> D e. ran ( x e. A |-> B ) )
10	4 5 9	syl2anc	|- ( ph -> D e. ran ( x e. A |-> B ) )
11	10	ne0d	|- ( ph -> ran ( x e. A |-> B ) =/= (/) )
12	1 3	rnmptbdd	|- ( ph -> E. y e. RR A. w e. ran ( x e. A |-> B ) w <_ y )
13	8 11 12 10	suprubd	|- ( ph -> D <_ sup ( ran ( x e. A |-> B ) , RR , < ) )