# Metamath Proof Explorer

## Theorem upbdrech2

Description: Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses upbdrech2.b
`|- ( ( ph /\ x e. A ) -> B e. RR )`
upbdrech2.bd
`|- ( ph -> E. y e. RR A. x e. A B <_ y )`
upbdrech2.c
`|- C = if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) )`
Assertion upbdrech2
`|- ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )`

### Proof

Step Hyp Ref Expression
1 upbdrech2.b
` |-  ( ( ph /\ x e. A ) -> B e. RR )`
2 upbdrech2.bd
` |-  ( ph -> E. y e. RR A. x e. A B <_ y )`
3 upbdrech2.c
` |-  C = if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) )`
4 iftrue
` |-  ( A = (/) -> if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) ) = 0 )`
5 0red
` |-  ( A = (/) -> 0 e. RR )`
6 4 5 eqeltrd
` |-  ( A = (/) -> if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) ) e. RR )`
7 6 adantl
` |-  ( ( ph /\ A = (/) ) -> if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) ) e. RR )`
8 simpr
` |-  ( ( ph /\ -. A = (/) ) -> -. A = (/) )`
9 8 iffalsed
` |-  ( ( ph /\ -. A = (/) ) -> if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) ) = sup ( { z | E. x e. A z = B } , RR , < ) )`
10 8 neqned
` |-  ( ( ph /\ -. A = (/) ) -> A =/= (/) )`
11 1 adantlr
` |-  ( ( ( ph /\ -. A = (/) ) /\ x e. A ) -> B e. RR )`
12 2 adantr
` |-  ( ( ph /\ -. A = (/) ) -> E. y e. RR A. x e. A B <_ y )`
13 eqid
` |-  sup ( { z | E. x e. A z = B } , RR , < ) = sup ( { z | E. x e. A z = B } , RR , < )`
14 10 11 12 13 upbdrech
` |-  ( ( ph /\ -. A = (/) ) -> ( sup ( { z | E. x e. A z = B } , RR , < ) e. RR /\ A. x e. A B <_ sup ( { z | E. x e. A z = B } , RR , < ) ) )`
15 14 simpld
` |-  ( ( ph /\ -. A = (/) ) -> sup ( { z | E. x e. A z = B } , RR , < ) e. RR )`
16 9 15 eqeltrd
` |-  ( ( ph /\ -. A = (/) ) -> if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) ) e. RR )`
17 7 16 pm2.61dan
` |-  ( ph -> if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) ) e. RR )`
18 3 17 eqeltrid
` |-  ( ph -> C e. RR )`
19 rzal
` |-  ( A = (/) -> A. x e. A B <_ C )`
20 19 adantl
` |-  ( ( ph /\ A = (/) ) -> A. x e. A B <_ C )`
21 14 simprd
` |-  ( ( ph /\ -. A = (/) ) -> A. x e. A B <_ sup ( { z | E. x e. A z = B } , RR , < ) )`
22 iffalse
` |-  ( -. A = (/) -> if ( A = (/) , 0 , sup ( { z | E. x e. A z = B } , RR , < ) ) = sup ( { z | E. x e. A z = B } , RR , < ) )`
23 3 22 syl5eq
` |-  ( -. A = (/) -> C = sup ( { z | E. x e. A z = B } , RR , < ) )`
24 23 breq2d
` |-  ( -. A = (/) -> ( B <_ C <-> B <_ sup ( { z | E. x e. A z = B } , RR , < ) ) )`
25 24 ralbidv
` |-  ( -. A = (/) -> ( A. x e. A B <_ C <-> A. x e. A B <_ sup ( { z | E. x e. A z = B } , RR , < ) ) )`
26 25 adantl
` |-  ( ( ph /\ -. A = (/) ) -> ( A. x e. A B <_ C <-> A. x e. A B <_ sup ( { z | E. x e. A z = B } , RR , < ) ) )`
27 21 26 mpbird
` |-  ( ( ph /\ -. A = (/) ) -> A. x e. A B <_ C )`
28 20 27 pm2.61dan
` |-  ( ph -> A. x e. A B <_ C )`
29 18 28 jca
` |-  ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )`