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→AB∪B=AB

Proof

Step Hyp Ref Expression
1 simp2 ⊢A∈ℝ*∧B∈ℝ*∧A<B→B∈ℝ*
2 iccid ⊢B∈ℝ*→BB=B
3 1 2 syl ⊢A∈ℝ*∧B∈ℝ*∧A<B→BB=B
4 3 uneq2d ⊢A∈ℝ*∧B∈ℝ*∧A<B→AB∪BB=AB∪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→AB∪BB=AB
19 5 1 1 6 7 18 syl32anc ⊢A∈ℝ*∧B∈ℝ*∧A<B→AB∪BB=AB
20 4 19 eqtr3d ⊢A∈ℝ*∧B∈ℝ*∧A<B→AB∪B=AB