Theorem suprubrnmpt

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

Proof

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