Theorem iccdifioo

Description: If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	iccdifioo	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = { 𝐴 , 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		prunioo	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( 𝐴 [,] 𝐵 ) )
2		uncom	⊢ ( ( 𝐴 (,) 𝐵 ) ∪ { 𝐴 , 𝐵 } ) = ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) )
3	1 2	eqtr3di	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 [,] 𝐵 ) = ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) )
4	3	difeq1d	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ∖ ( 𝐴 (,) 𝐵 ) ) )
5		difun2	⊢ ( ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) )
6	5	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( { 𝐴 , 𝐵 } ∪ ( 𝐴 (,) 𝐵 ) ) ∖ ( 𝐴 (,) 𝐵 ) ) = ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) ) )
7		incom	⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ( { 𝐴 , 𝐵 } ∩ ( 𝐴 (,) 𝐵 ) )
8		iooinlbub	⊢ ( ( 𝐴 (,) 𝐵 ) ∩ { 𝐴 , 𝐵 } ) = ∅
9	7 8	eqtr3i	⊢ ( { 𝐴 , 𝐵 } ∩ ( 𝐴 (,) 𝐵 ) ) = ∅
10		disj3	⊢ ( ( { 𝐴 , 𝐵 } ∩ ( 𝐴 (,) 𝐵 ) ) = ∅ ↔ { 𝐴 , 𝐵 } = ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) ) )
11	9 10	mpbi	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) )
12	11	eqcomi	⊢ ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) ) = { 𝐴 , 𝐵 }
13	12	a1i	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( { 𝐴 , 𝐵 } ∖ ( 𝐴 (,) 𝐵 ) ) = { 𝐴 , 𝐵 } )
14	4 6 13	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = { 𝐴 , 𝐵 } )