Metamath Proof Explorer

Theorem icodisj

Description: Adjacent left-closed right-open real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion icodisj ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) )
2 elico1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
3 2 3adant3 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) ) )
4 3 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → ( 𝑥 ∈ ℝ* ∧ 𝐴 ≤ 𝑥 ∧ 𝑥 < 𝐵 ) )
5 4 simp3d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ) → 𝑥 < 𝐵 )
6 5 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) ) → 𝑥 < 𝐵 )
7 elico1 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶 ) ) )
8 7 3adant1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶 ) ) )
9 8 biimpa ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → ( 𝑥 ∈ ℝ* ∧ 𝐵 ≤ 𝑥 ∧ 𝑥 < 𝐶 ) )
10 9 simp2d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → 𝐵 ≤ 𝑥 )
11 simpl2 ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → 𝐵 ∈ ℝ* )
12 9 simp1d ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → 𝑥 ∈ ℝ* )
13 11 12 xrlenltd ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → ( 𝐵 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐵 ) )
14 10 13 mpbid ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → ¬ 𝑥 < 𝐵 )
15 14 adantrl ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) ) → ¬ 𝑥 < 𝐵 )
16 6 15 pm2.65da ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ¬ ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) )
17 16 pm2.21d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝑥 ∈ ( 𝐵 [,) 𝐶 ) ) → 𝑥 ∈ ∅ ) )
18 1 17 syl5bi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝑥 ∈ ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) → 𝑥 ∈ ∅ ) )
19 18 ssrdv ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) ⊆ ∅ )
20 ss0 ⊢ ( ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) ⊆ ∅ → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ )
21 19 20 syl ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( ( 𝐴 [,) 𝐵 ) ∩ ( 𝐵 [,) 𝐶 ) ) = ∅ )