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

Metamath Proof Explorer

Theorem joiniooico

Description: Disjoint joining an open interval with a closed-below, open-above interval to form a closed-below, open-above interval. (Contributed by Thierry Arnoux, 26-Sep-2017)

		Ref	Expression
	Assertion	joiniooico	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ ∧ ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ioo	⊢ (,) = ( 𝑎 ∈ ℝ^* , 𝑏 ∈ ℝ^* ↦ { 𝑥 ∈ ℝ^* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } )
2		df-ico	⊢ [,) = ( 𝑎 ∈ ℝ^* , 𝑏 ∈ ℝ^* ↦ { 𝑥 ∈ ℝ^* ∣ ( 𝑎 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) } )
3		xrlenlt	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝐵 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐵 ) )
4	1 2 3	ixxdisj	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ )
5	4	adantr	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ )
6		xrltletr	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) → ( ( 𝑤 < 𝐵 ∧ 𝐵 ≤ 𝐶 ) → 𝑤 < 𝐶 ) )
7		xrltletr	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( ( 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝑤 ) → 𝐴 < 𝑤 ) )
8	1 2 3 1 6 7	ixxun	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) )
9	5 8	jca	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ ∧ ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) ) )