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