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

Metamath Proof Explorer

Theorem supicclub

Description: The supremum of a bounded set of real numbers is the least upper bound. (Contributed by Thierry Arnoux, 23-May-2019)

Ref Expression
Hypotheses supicc.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
supicc.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
supicc.3 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐵 [,] 𝐶 ) )
supicc.4 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
supiccub.1 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
Assertion supicclub ( 𝜑 → ( 𝐷 < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 𝐷 < 𝑧 ) )

Proof

Step Hyp Ref Expression
1 supicc.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2 supicc.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 supicc.3 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐵 [,] 𝐶 ) )
4 supicc.4 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5 supiccub.1 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
6 iccssre ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
7 1 2 6 syl2anc ⊢ ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
8 3 7 sstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
10 9 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
12 11 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ* )
13 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝐵 [,] 𝐶 ) )
14 iccleub ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝑥 ≤ 𝐶 )
15 10 12 13 14 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ 𝐶 )
16 15 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐶 )
17 brralrspcev ⊢ ( ( 𝐶 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝐶 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 )
18 2 16 17 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 )
19 8 5 sseldd ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
20 suprlub ⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 ) ∧ 𝐷 ∈ ℝ ) → ( 𝐷 < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 𝐷 < 𝑧 ) )
21 8 4 18 19 20 syl31anc ⊢ ( 𝜑 → ( 𝐷 < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 𝐷 < 𝑧 ) )