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 → A B ∖ A B = A B

Proof

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