Theorem iccsupr

Description: A nonempty subset of a closed real interval satisfies the conditions for the existence of its supremum (see suprcl ). (Contributed by Paul Chapman, 21-Jan-2008)

	Ref	Expression
Assertion	iccsupr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ 𝑆 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
2		sstr	⊢ ( ( 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → 𝑆 ⊆ ℝ )
3	2	ancoms	⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) → 𝑆 ⊆ ℝ )
4	1 3	sylan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) → 𝑆 ⊆ ℝ )
5	4	3adant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ 𝑆 ) → 𝑆 ⊆ ℝ )
6		ne0i	⊢ ( 𝐶 ∈ 𝑆 → 𝑆 ≠ ∅ )
7	6	3ad2ant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ 𝑆 ) → 𝑆 ≠ ∅ )
8		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) → 𝐵 ∈ ℝ )
9		ssel	⊢ ( 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) )
10		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
11	10	biimpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
12	9 11	sylan9r	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ 𝑆 → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
13	12	imp	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) )
14	13	simp3d	⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ≤ 𝐵 )
15	14	ralrimiva	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 )
16		brralrspcev	⊢ ( ( 𝐵 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 )
17	8 15 16	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 )
18	17	3adant3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ 𝑆 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 )
19	5 7 18	3jca	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ 𝑆 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )