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

Metamath Proof Explorer

Theorem supicclub2

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 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
supicclub2.1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ≤ 𝐷 )
Assertion supicclub2 ( 𝜑 → sup ( 𝐴 , ℝ , < ) ≤ 𝐷 )

Proof

Step Hyp Ref Expression
1 supicc.1 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
2 supicc.2 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3 supicc.3 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐵 [,] 𝐶 ) )
4 supicc.4 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5 supiccub.1 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
6 supicclub2.1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ≤ 𝐷 )
7 iccssxr ⊢ ( 𝐵 [,] 𝐶 ) ⊆ ℝ*
8 1 2 3 4 supicc ⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ( 𝐵 [,] 𝐶 ) )
9 7 8 sselid ⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ∈ ℝ* )
10 3 7 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
11 10 5 sseldd ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
12 10 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ ℝ* )
13 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐷 ∈ ℝ* )
14 12 13 xrlenltd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑧 ≤ 𝐷 ↔ ¬ 𝐷 < 𝑧 ) )
15 6 14 mpbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ¬ 𝐷 < 𝑧 )
16 15 nrexdv ⊢ ( 𝜑 → ¬ ∃ 𝑧 ∈ 𝐴 𝐷 < 𝑧 )
17 1 2 3 4 5 supicclub ⊢ ( 𝜑 → ( 𝐷 < sup ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 𝐷 < 𝑧 ) )
18 16 17 mtbird ⊢ ( 𝜑 → ¬ 𝐷 < sup ( 𝐴 , ℝ , < ) )
19 9 11 18 xrnltled ⊢ ( 𝜑 → sup ( 𝐴 , ℝ , < ) ≤ 𝐷 )