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

Proof

Step	Hyp	Ref	Expression
1		un23	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) 𝐶 ) ) = ( ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 (,) 𝐶 ) ) ∪ { 𝐵 } )
2		unundir	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ ( 𝐵 (,) 𝐶 ) ) ∪ { 𝐵 } ) = ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( ( 𝐵 (,) 𝐶 ) ∪ { 𝐵 } ) )
3		uncom	⊢ ( ( 𝐵 (,) 𝐶 ) ∪ { 𝐵 } ) = ( { 𝐵 } ∪ ( 𝐵 (,) 𝐶 ) )
4	3	uneq2i	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( ( 𝐵 (,) 𝐶 ) ∪ { 𝐵 } ) ) = ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( 𝐵 (,) 𝐶 ) ) )
5	1 2 4	3eqtrri	⊢ ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( 𝐵 (,) 𝐶 ) ) ) = ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) 𝐶 ) )
6		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐴 ∈ ℝ* )
7		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 ∈ ℝ* )
8		simprl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐴 < 𝐵 )
9		ioounsn	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
10	6 7 8 9	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) = ( 𝐴 (,] 𝐵 ) )
11		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐶 ∈ ℝ* )
12		simprr	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → 𝐵 < 𝐶 )
13		snunioo	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝐵 < 𝐶 ) → ( { 𝐵 } ∪ ( 𝐵 (,) 𝐶 ) ) = ( 𝐵 [,) 𝐶 ) )
14	7 11 12 13	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( { 𝐵 } ∪ ( 𝐵 (,) 𝐶 ) ) = ( 𝐵 [,) 𝐶 ) )
15	10 14	uneq12d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( { 𝐵 } ∪ ( 𝐵 (,) 𝐶 ) ) ) = ( ( 𝐴 (,] 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) )
16		ioojoin	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐵 } ) ∪ ( 𝐵 (,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) )
17	5 15 16	3eqtr3a	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 < 𝐵 ∧ 𝐵 < 𝐶 ) ) → ( ( 𝐴 (,] 𝐵 ) ∪ ( 𝐵 [,) 𝐶 ) ) = ( 𝐴 (,) 𝐶 ) )