# 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 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
upbdrech2.bd ${⊢}{\phi }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
upbdrech2.c ${⊢}{C}=if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)$
Assertion upbdrech2 ${⊢}{\phi }\to \left({C}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}\right)$

### Proof

Step Hyp Ref Expression
1 upbdrech2.b ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
2 upbdrech2.bd ${⊢}{\phi }\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
3 upbdrech2.c ${⊢}{C}=if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)$
4 iftrue ${⊢}{A}=\varnothing \to if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)=0$
5 0red ${⊢}{A}=\varnothing \to 0\in ℝ$
6 4 5 eqeltrd ${⊢}{A}=\varnothing \to if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)\in ℝ$
7 6 adantl ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)\in ℝ$
8 simpr ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to ¬{A}=\varnothing$
9 8 iffalsed ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)=sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)$
10 8 neqned ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to {A}\ne \varnothing$
11 1 adantlr ${⊢}\left(\left({\phi }\wedge ¬{A}=\varnothing \right)\wedge {x}\in {A}\right)\to {B}\in ℝ$
12 2 adantr ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to \exists {y}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {y}$
13 eqid ${⊢}sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)=sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)$
14 10 11 12 13 upbdrech ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to \left(sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)$
15 14 simpld ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\in ℝ$
16 9 15 eqeltrd ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)\in ℝ$
17 7 16 pm2.61dan ${⊢}{\phi }\to if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)\in ℝ$
18 3 17 eqeltrid ${⊢}{\phi }\to {C}\in ℝ$
19 rzal ${⊢}{A}=\varnothing \to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}$
20 19 adantl ${⊢}\left({\phi }\wedge {A}=\varnothing \right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}$
21 14 simprd ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)$
22 iffalse ${⊢}¬{A}=\varnothing \to if\left({A}=\varnothing ,0,sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)=sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)$
23 3 22 syl5eq ${⊢}¬{A}=\varnothing \to {C}=sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)$
24 23 breq2d ${⊢}¬{A}=\varnothing \to \left({B}\le {C}↔{B}\le sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)$
25 24 ralbidv ${⊢}¬{A}=\varnothing \to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)$
26 25 adantl ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le sup\left(\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}={B}\right\},ℝ,<\right)\right)$
27 21 26 mpbird ${⊢}\left({\phi }\wedge ¬{A}=\varnothing \right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}$
28 20 27 pm2.61dan ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}$
29 18 28 jca ${⊢}{\phi }\to \left({C}\in ℝ\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\le {C}\right)$