Metamath Proof Explorer

Theorem ioojoin

Description: Join two open intervals to create a third. (Contributed by NM, 11-Aug-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion ioojoin ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B ∪ B C = A C

Proof

Step Hyp Ref Expression
1 unass ⊢ A B ∪ B ∪ B C = A B ∪ B ∪ B C
2 snunioo ⊢ B ∈ ℝ * ∧ C ∈ ℝ * ∧ B < C → B ∪ B C = B C
3 2 3expa ⊢ B ∈ ℝ * ∧ C ∈ ℝ * ∧ B < C → B ∪ B C = B C
4 3 3adantl1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ B < C → B ∪ B C = B C
5 4 adantrl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → B ∪ B C = B C
6 5 uneq2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B ∪ B C = A B ∪ B C
7 df-ioo ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x < z ∧ z < y
8 df-ico ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z < y
9 xrlenlt ⊢ B ∈ ℝ * ∧ w ∈ ℝ * → B ≤ w ↔ ¬ w < B
10 xrlttr ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * → w < B ∧ B < C → w < C
11 xrltletr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ w ∈ ℝ * → A < B ∧ B ≤ w → A < w
12 7 8 9 7 10 11 ixxun ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B C = A C
13 6 12 eqtrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B ∪ B C = A C
14 1 13 syl5eq ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B ∪ B C = A C