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 ( ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵𝐵𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ ∧ ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) ) )