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 ( 𝐴 , ℝ , < ) ↔ ∃ 𝑧 ∈ 𝐴 𝐷 < 𝑧 ) )