Theorem icoun

Description: The union of two adjacent left-closed right-open real intervals is a left-closed right-open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

	Ref	Expression
Assertion	icoun	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 [,) 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ico	⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
2		xrlenlt	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐵 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐵 ) )
3		xrltletr	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑤 < 𝐵 ∧ 𝐵 ≤ 𝐶 ) → 𝑤 < 𝐶 ) )
4		xrletr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝑤 ) → 𝐴 ≤ 𝑤 ) )
5	1 1 2 1 3 4	ixxun	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 [,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 [,) 𝐶 ) )