Metamath Proof Explorer

Theorem snunico

Description: The closure of the open end of a right-open real interval. (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion snunico ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A B ∪ B = A B

Proof

Step Hyp Ref Expression
1 simp2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → B ∈ ℝ *
2 iccid ⊢ B ∈ ℝ * → B B = B
3 1 2 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → B B = B
4 3 uneq2d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A B ∪ B B = A B ∪ B
5 simp1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A ∈ ℝ *
6 simp3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A ≤ B
7 1 xrleidd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → B ≤ B
8 df-ico ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z < y
9 df-icc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x ≤ z ∧ z ≤ y
10 xrlenlt ⊢ B ∈ ℝ * ∧ w ∈ ℝ * → B ≤ w ↔ ¬ w < B
11 xrltle ⊢ w ∈ ℝ * ∧ B ∈ ℝ * → w < B → w ≤ B
12 11 3adant3 ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * → w < B → w ≤ B
13 12 adantrd ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * → w < B ∧ B ≤ B → w ≤ B
14 xrletr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ w ∈ ℝ * → A ≤ B ∧ B ≤ w → A ≤ w
15 8 9 10 9 13 14 ixxun ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B ∧ B ≤ B → A B ∪ B B = A B
16 5 1 1 6 7 15 syl32anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A B ∪ B B = A B
17 4 16 eqtr3d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A B ∪ B = A B