Metamath Proof Explorer


Theorem icossioo

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 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐶𝐷𝐵 ) ) → ( 𝐶 [,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-ioo (,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥𝑥 < 𝑏 ) } )
2 df-ico [,) = ( 𝑎 ∈ ℝ* , 𝑏 ∈ ℝ* ↦ { 𝑥 ∈ ℝ* ∣ ( 𝑎𝑥𝑥 < 𝑏 ) } )
3 xrltletr ( ( 𝐴 ∈ ℝ*𝐶 ∈ ℝ*𝑤 ∈ ℝ* ) → ( ( 𝐴 < 𝐶𝐶𝑤 ) → 𝐴 < 𝑤 ) )
4 xrltletr ( ( 𝑤 ∈ ℝ*𝐷 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝑤 < 𝐷𝐷𝐵 ) → 𝑤 < 𝐵 ) )
5 1 2 3 4 ixxss12 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) ∧ ( 𝐴 < 𝐶𝐷𝐵 ) ) → ( 𝐶 [,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )