This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( ( 𝐴 [,] 𝐵 ) ∖ ( 𝐴 (,) 𝐵 ) ) = { 𝐴 , 𝐵 } )