Metamath Proof Explorer


Theorem suprclrnmpt

Description: Closure of the indexed supremum of a nonempty bounded set of reals. Range of a function in maps-to notation can be used, to express an indexed supremum. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses suprclrnmpt.x
|- F/ x ph
suprclrnmpt.n
|- ( ph -> A =/= (/) )
suprclrnmpt.b
|- ( ( ph /\ x e. A ) -> B e. RR )
suprclrnmpt.y
|- ( ph -> E. y e. RR A. x e. A B <_ y )
Assertion suprclrnmpt
|- ( ph -> sup ( ran ( x e. A |-> B ) , RR , < ) e. RR )

Proof

Step Hyp Ref Expression
1 suprclrnmpt.x
 |-  F/ x ph
2 suprclrnmpt.n
 |-  ( ph -> A =/= (/) )
3 suprclrnmpt.b
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 suprclrnmpt.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 6 7 8 suprcld
 |-  ( ph -> sup ( ran ( x e. A |-> B ) , RR , < ) e. RR )