Metamath Proof Explorer

Theorem ioounsn

Description: The union of an open interval with its upper endpoint is a left-open right-closed interval. (Contributed by Jon Pennant, 8-Jun-2019)

Ref Expression
Assertion ioounsn ⊢ 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-ioo ⊢ . = 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 df-ioc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x < z ∧ z ≤ y
12 simpl1 ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * ∧ w < B ∧ B ≤ B → w ∈ ℝ *
13 simpl2 ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * ∧ w < B ∧ B ≤ B → B ∈ ℝ *
14 simprl ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * ∧ w < B ∧ B ≤ B → w < B
15 12 13 14 xrltled ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * ∧ w < B ∧ B ≤ B → w ≤ B
16 15 ex ⊢ w ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * → w < B ∧ B ≤ B → w ≤ B
17 xrltletr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ w ∈ ℝ * → A < B ∧ B ≤ w → A < w
18 8 9 10 11 16 17 ixxun ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B ∧ B ≤ B → A B ∪ B B = A B
19 5 1 1 6 7 18 syl32anc ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B → A B ∪ B B = A B
20 4 19 eqtr3d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B → A B ∪ B = A B