Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  upbdrech2 Structured version   Visualization version   Unicode version

Theorem upbdrech2 37526
 Description: Choice of an upper bound for a possibly empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
upbdrech2.b
upbdrech2.bd
upbdrech2.c
Assertion
Ref Expression
upbdrech2
Distinct variable groups:   ,,,   ,,   ,,
Allowed substitution hints:   ()   ()   (,,)

Proof of Theorem upbdrech2
StepHypRef Expression
1 upbdrech2.c . . 3
2 iftrue 3887 . . . . . 6
3 0red 9644 . . . . . 6
42, 3eqeltrd 2529 . . . . 5
54adantl 468 . . . 4
6 simpr 463 . . . . . 6
76iffalsed 3892 . . . . 5
86neqned 2631 . . . . . . 7
9 upbdrech2.b . . . . . . . 8
109adantlr 721 . . . . . . 7
11 upbdrech2.bd . . . . . . . 8
1211adantr 467 . . . . . . 7
13 eqid 2451 . . . . . . 7
148, 10, 12, 13upbdrech 37523 . . . . . 6
1514simpld 461 . . . . 5
167, 15eqeltrd 2529 . . . 4
175, 16pm2.61dan 800 . . 3
181, 17syl5eqel 2533 . 2
19 rzal 3871 . . . 4