This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,) B ) u. { B } ) = ( A [,] B ) )

Proof

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