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 ℝ\forall x\in AB\le y$$
	upbdrech2.c	$$⊢C=if\left(A=\varnothing ,0,sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)$$
Assertion	upbdrech2	$$⊢\phi \to \left(C\in ℝ\wedge \forall x\in AB\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 ℝ\forall x\in AB\le y$$
3		upbdrech2.c	$$⊢C=if\left(A=\varnothing ,0,sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)$$
4		iftrue	$$⊢A=\varnothing \to if\left(A=\varnothing ,0,sup\left(\left\{z|\exists x\in Az=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 Az=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 Az=B\right\},ℝ,<\right)\right)\in ℝ$$
8		simpr	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \neg A=\varnothing$$
9	8	iffalsed	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to if\left(A=\varnothing ,0,sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)=sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)$$
10	8	neqned	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to A\ne \varnothing$$
11	1	adantlr	$$⊢\left(\left(\phi \wedge \neg A=\varnothing \right)\wedge x\in A\right)\to B\in ℝ$$
12	2	adantr	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \exists y\in ℝ\forall x\in AB\le y$$
13		eqid	$$⊢sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)=sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)$$
14	10 11 12 13	upbdrech	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \left(sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\in ℝ\wedge \forall x\in AB\le sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)$$
15	14	simpld	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\in ℝ$$
16	9 15	eqeltrd	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to if\left(A=\varnothing ,0,sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)\in ℝ$$
17	7 16	pm2.61dan	$$⊢\phi \to if\left(A=\varnothing ,0,sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)\in ℝ$$
18	3 17	eqeltrid	$$⊢\phi \to C\in ℝ$$
19		rzal	$$⊢A=\varnothing \to \forall x\in AB\le C$$
20	19	adantl	$$⊢\left(\phi \wedge A=\varnothing \right)\to \forall x\in AB\le C$$
21	14	simprd	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \forall x\in AB\le sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)$$
22		iffalse	$$⊢\neg A=\varnothing \to if\left(A=\varnothing ,0,sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)=sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)$$
23	3 22	syl5eq	$$⊢\neg A=\varnothing \to C=sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)$$
24	23	breq2d	$$⊢\neg A=\varnothing \to \left(B\le C\leftrightarrow B\le sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)$$
25	24	ralbidv	$$⊢\neg A=\varnothing \to \left(\forall x\in AB\le C\leftrightarrow \forall x\in AB\le sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)$$
26	25	adantl	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \left(\forall x\in AB\le C\leftrightarrow \forall x\in AB\le sup\left(\left\{z|\exists x\in Az=B\right\},ℝ,<\right)\right)$$
27	21 26	mpbird	$$⊢\left(\phi \wedge \neg A=\varnothing \right)\to \forall x\in AB\le C$$
28	20 27	pm2.61dan	$$⊢\phi \to \forall x\in AB\le C$$
29	18 28	jca	$$⊢\phi \to \left(C\in ℝ\wedge \forall x\in AB\le C\right)$$