Metamath Proof Explorer


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