This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
upbdrech2.bd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
upbdrech2.c ⊢ 𝐶 = if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
Assertion upbdrech2 ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 upbdrech2.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
2 upbdrech2.bd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
3 upbdrech2.c ⊢ 𝐶 = if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
4 iftrue ⊢ ( 𝐴 = ∅ → if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) = 0 )
5 0red ⊢ ( 𝐴 = ∅ → 0 ∈ ℝ )
6 4 5 eqeltrd ⊢ ( 𝐴 = ∅ → if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) ∈ ℝ )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) ∈ ℝ )
8 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ¬ 𝐴 = ∅ )
9 8 iffalsed ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) = sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
10 8 neqned ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → 𝐴 ≠ ∅ )
11 1 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
12 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 )
13 eqid ⊢ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) = sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < )
14 10 11 12 13 upbdrech ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ( sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) )
15 14 simpld ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ∈ ℝ )
16 9 15 eqeltrd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) ∈ ℝ )
17 7 16 pm2.61dan ⊢ ( 𝜑 → if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) ∈ ℝ )
18 3 17 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
19 rzal ⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
21 14 simprd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
22 iffalse ⊢ ( ¬ 𝐴 = ∅ → if ( 𝐴 = ∅ , 0 , sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) = sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
23 3 22 eqtrid ⊢ ( ¬ 𝐴 = ∅ → 𝐶 = sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) )
24 23 breq2d ⊢ ( ¬ 𝐴 = ∅ → ( 𝐵 ≤ 𝐶 ↔ 𝐵 ≤ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) )
25 24 ralbidv ⊢ ( ¬ 𝐴 = ∅ → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ sup ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = 𝐵 } , ℝ , < ) ) )
27 21 26 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐴 = ∅ ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
28 20 27 pm2.61dan ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 )
29 18 28 jca ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝐶 ) )