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→AB∪BC=AC

Proof

Step Hyp Ref Expression
1 un23 ⊢AB∪B∪BC=AB∪BC∪B
2 unundir ⊢AB∪BC∪B=AB∪B∪BC∪B
3 uncom ⊢BC∪B=B∪BC
4 3 uneq2i ⊢AB∪B∪BC∪B=AB∪B∪B∪BC
5 1 2 4 3eqtrri ⊢AB∪B∪B∪BC=AB∪B∪BC
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→AB∪B=AB
10 6 7 8 9 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B<C→AB∪B=AB
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∪BC=BC
14 7 11 12 13 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B<C→B∪BC=BC
15 10 14 uneq12d ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B<C→AB∪B∪B∪BC=AB∪BC
16 ioojoin ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B<C→AB∪B∪BC=AC
17 5 15 16 3eqtr3a ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧A<B∧B<C→AB∪BC=AC