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

Metamath Proof Explorer

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 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑆 ⊆ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 ∈ 𝑆 ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )