Metamath Proof Explorer


Theorem snunioo

Description: The closure of one end of an open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)

Ref Expression
Assertion snunioo
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A e. RR* )
2 iccid
 |-  ( A e. RR* -> ( A [,] A ) = { A } )
3 1 2 syl
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( A [,] A ) = { A } )
4 3 uneq1d
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A [,] A ) u. ( A (,) B ) ) = ( { A } u. ( A (,) B ) ) )
5 simp2
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> B e. RR* )
6 1 xrleidd
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A <_ A )
7 simp3
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> A < B )
8 df-icc
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
9 df-ioo
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
10 xrltnle
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w <-> -. w <_ A ) )
11 df-ico
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
12 xrlelttr
 |-  ( ( w e. RR* /\ A e. RR* /\ B e. RR* ) -> ( ( w <_ A /\ A < B ) -> w < B ) )
13 xrltle
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A <_ w ) )
14 13 3adant1
 |-  ( ( A e. RR* /\ A e. RR* /\ w e. RR* ) -> ( A < w -> A <_ w ) )
15 14 adantld
 |-  ( ( A e. RR* /\ A e. RR* /\ w e. RR* ) -> ( ( A <_ A /\ A < w ) -> A <_ w ) )
16 8 9 10 11 12 15 ixxun
 |-  ( ( ( A e. RR* /\ A e. RR* /\ B e. RR* ) /\ ( A <_ A /\ A < B ) ) -> ( ( A [,] A ) u. ( A (,) B ) ) = ( A [,) B ) )
17 1 1 5 6 7 16 syl32anc
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A [,] A ) u. ( A (,) B ) ) = ( A [,) B ) )
18 4 17 eqtr3d
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( { A } u. ( A (,) B ) ) = ( A [,) B ) )