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 ⊢φ∧x∈A→B∈ℝ
upbdrech2.bd ⊢φ→∃y∈ℝ∀x∈AB≤y
upbdrech2.c ⊢C=ifA=∅0supz|∃x∈Az=Bℝ<
Assertion upbdrech2 ⊢φ→C∈ℝ∧∀x∈AB≤C

Proof

Step Hyp Ref Expression
1 upbdrech2.b ⊢φ∧x∈A→B∈ℝ
2 upbdrech2.bd ⊢φ→∃y∈ℝ∀x∈AB≤y
3 upbdrech2.c ⊢C=ifA=∅0supz|∃x∈Az=Bℝ<
4 iftrue ⊢A=∅→ifA=∅0supz|∃x∈Az=Bℝ<=0
5 0red ⊢A=∅→0∈ℝ
6 4 5 eqeltrd ⊢A=∅→ifA=∅0supz|∃x∈Az=Bℝ<∈ℝ
7 6 adantl ⊢φ∧A=∅→ifA=∅0supz|∃x∈Az=Bℝ<∈ℝ
8 simpr ⊢φ∧¬A=∅→¬A=∅
9 8 iffalsed ⊢φ∧¬A=∅→ifA=∅0supz|∃x∈Az=Bℝ<=supz|∃x∈Az=Bℝ<
10 8 neqned ⊢φ∧¬A=∅→A≠∅
11 1 adantlr ⊢φ∧¬A=∅∧x∈A→B∈ℝ
12 2 adantr ⊢φ∧¬A=∅→∃y∈ℝ∀x∈AB≤y
13 eqid ⊢supz|∃x∈Az=Bℝ<=supz|∃x∈Az=Bℝ<
14 10 11 12 13 upbdrech ⊢φ∧¬A=∅→supz|∃x∈Az=Bℝ<∈ℝ∧∀x∈AB≤supz|∃x∈Az=Bℝ<
15 14 simpld ⊢φ∧¬A=∅→supz|∃x∈Az=Bℝ<∈ℝ
16 9 15 eqeltrd ⊢φ∧¬A=∅→ifA=∅0supz|∃x∈Az=Bℝ<∈ℝ
17 7 16 pm2.61dan ⊢φ→ifA=∅0supz|∃x∈Az=Bℝ<∈ℝ
18 3 17 eqeltrid ⊢φ→C∈ℝ
19 rzal ⊢A=∅→∀x∈AB≤C
20 19 adantl ⊢φ∧A=∅→∀x∈AB≤C
21 14 simprd ⊢φ∧¬A=∅→∀x∈AB≤supz|∃x∈Az=Bℝ<
22 iffalse ⊢¬A=∅→ifA=∅0supz|∃x∈Az=Bℝ<=supz|∃x∈Az=Bℝ<
23 3 22 eqtrid ⊢¬A=∅→C=supz|∃x∈Az=Bℝ<
24 23 breq2d ⊢¬A=∅→B≤C↔B≤supz|∃x∈Az=Bℝ<
25 24 ralbidv ⊢¬A=∅→∀x∈AB≤C↔∀x∈AB≤supz|∃x∈Az=Bℝ<
26 25 adantl ⊢φ∧¬A=∅→∀x∈AB≤C↔∀x∈AB≤supz|∃x∈Az=Bℝ<
27 21 26 mpbird ⊢φ∧¬A=∅→∀x∈AB≤C
28 20 27 pm2.61dan ⊢φ→∀x∈AB≤C
29 18 28 jca ⊢φ→C∈ℝ∧∀x∈AB≤C