Metamath Proof Explorer


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 , < ) )