Metamath Proof Explorer

Theorem iocunico

Description: Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019)

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

Proof

Step Hyp Ref Expression
1 un23 ⊢ A B ∪ B ∪ B C = A B ∪ B C ∪ B
2 unundir ⊢ A B ∪ B C ∪ B = A B ∪ B ∪ B C ∪ B
3 uncom ⊢ B C ∪ B = B ∪ B C
4 3 uneq2i ⊢ A B ∪ B ∪ B C ∪ B = A B ∪ B ∪ B ∪ B C
5 1 2 4 3eqtrri ⊢ A B ∪ B ∪ B ∪ B C = A B ∪ B ∪ B C
6 simpl1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A ∈ ℝ *
7 simpl2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → B ∈ ℝ *
8 simprl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A < B
9 ioounsn ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B → A B ∪ B = A B
10 6 7 8 9 syl3anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B = A B
11 simpl3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → C ∈ ℝ *
12 simprr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → B < C
13 snunioo ⊢ B ∈ ℝ * ∧ C ∈ ℝ * ∧ B < C → B ∪ B C = B C
14 7 11 12 13 syl3anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → B ∪ B C = B C
15 10 14 uneq12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B ∪ B ∪ B C = A B ∪ B C
16 ioojoin ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B ∪ B C = A C
17 5 15 16 3eqtr3a ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ C ∈ ℝ * ∧ A < B ∧ B < C → A B ∪ B C = A C