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 ( 𝐴 , ℝ , < ) ≤ 𝐷 )