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 ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∖AB=AB

Proof

Step Hyp Ref Expression
1 prunioo ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∪AB=AB
2 uncom ⊢AB∪AB=AB∪AB
3 1 2 eqtr3di ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB=AB∪AB
4 3 difeq1d ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∖AB=AB∪AB∖AB
5 difun2 ⊢AB∪AB∖AB=AB∖AB
6 5 a1i ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∪AB∖AB=AB∖AB
7 incom ⊢AB∩AB=AB∩AB
8 iooinlbub ⊢AB∩AB=∅
9 7 8 eqtr3i ⊢AB∩AB=∅
10 disj3 ⊢AB∩AB=∅↔AB=AB∖AB
11 9 10 mpbi ⊢AB=AB∖AB
12 11 eqcomi ⊢AB∖AB=AB
13 12 a1i ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∖AB=AB
14 4 6 13 3eqtrd ⊢A∈ℝ*∧B∈ℝ*∧A≤B→AB∖AB=AB