Description: Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 29-Mar-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | icossioo | ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → ( 𝐶 [,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioo | ⊢ (,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } ) | |
2 | df-ico | ⊢ [,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑥 ∈ ℝ* ∣ ( 𝑎 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) } ) | |
3 | xrltletr | ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝐴 < 𝐶 ∧ 𝐶 ≤ 𝑤 ) → 𝐴 < 𝑤 ) ) | |
4 | xrltletr | ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝑤 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) → 𝑤 < 𝐵 ) ) | |
5 | 1 2 3 4 | ixxss12 | ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → ( 𝐶 [,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) |