# 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 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to \left[{A},{B}\right)\cup \left\{{B}\right\}=\left[{A},{B}\right]$

### Proof

Step Hyp Ref Expression
1 simp2 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to {B}\in {ℝ}^{*}$
2 iccid ${⊢}{B}\in {ℝ}^{*}\to \left[{B},{B}\right]=\left\{{B}\right\}$
3 1 2 syl ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to \left[{B},{B}\right]=\left\{{B}\right\}$
4 3 uneq2d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to \left[{A},{B}\right)\cup \left[{B},{B}\right]=\left[{A},{B}\right)\cup \left\{{B}\right\}$
5 simp1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to {A}\in {ℝ}^{*}$
6 simp3 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to {A}\le {B}$
7 1 xrleidd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to {B}\le {B}$
8 df-ico ${⊢}\left[.\right)=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}<{y}\right)\right\}\right)$
9 df-icc ${⊢}\left[.\right]=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}\le {z}\wedge {z}\le {y}\right)\right\}\right)$
10 xrlenlt ${⊢}\left({B}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left({B}\le {w}↔¬{w}<{B}\right)$
11 xrltle ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}<{B}\to {w}\le {B}\right)$
12 11 3adant3 ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({w}<{B}\to {w}\le {B}\right)$
13 12 adantrd ${⊢}\left({w}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({w}<{B}\wedge {B}\le {B}\right)\to {w}\le {B}\right)$
14 xrletr ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {w}\in {ℝ}^{*}\right)\to \left(\left({A}\le {B}\wedge {B}\le {w}\right)\to {A}\le {w}\right)$
15 8 9 10 9 13 14 ixxun ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({A}\le {B}\wedge {B}\le {B}\right)\right)\to \left[{A},{B}\right)\cup \left[{B},{B}\right]=\left[{A},{B}\right]$
16 5 1 1 6 7 15 syl32anc ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to \left[{A},{B}\right)\cup \left[{B},{B}\right]=\left[{A},{B}\right]$
17 4 16 eqtr3d ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}\le {B}\right)\to \left[{A},{B}\right)\cup \left\{{B}\right\}=\left[{A},{B}\right]$