Metamath Proof Explorer

Theorem snunioc

Description: The closure of the open end of a left-open real interval. (Contributed by Thierry Arnoux, 28-Mar-2017)

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

Proof

Step Hyp Ref Expression
1 iccid 
 |-  ( A e. RR* -> ( A [,] A ) = { A } )
2 1 3ad2ant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A [,] A ) = { A } )
3 2 uneq1d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] A ) u. ( A (,] B ) ) = ( { A } u. ( A (,] B ) ) )
4 simp1 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. RR* )
5 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. RR* )
6 xrleid 
 |-  ( A e. RR* -> A <_ A )
7 6 3ad2ant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ A )
8 simp3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ B )
9 df-icc 
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
10 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
11 xrltnle 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w <-> -. w <_ A ) )
12 xrletr 
 |-  ( ( w e. RR* /\ A e. RR* /\ B e. RR* ) -> ( ( w <_ A /\ A <_ B ) -> w <_ B ) )
13 simpl1 
 |-  ( ( ( A e. RR* /\ A e. RR* /\ w e. RR* ) /\ ( A <_ A /\ A < w ) ) -> A e. RR* )
14 simpl3 
 |-  ( ( ( A e. RR* /\ A e. RR* /\ w e. RR* ) /\ ( A <_ A /\ A < w ) ) -> w e. RR* )
15 simprr 
 |-  ( ( ( A e. RR* /\ A e. RR* /\ w e. RR* ) /\ ( A <_ A /\ A < w ) ) -> A < w )
16 13 14 15 xrltled 
 |-  ( ( ( A e. RR* /\ A e. RR* /\ w e. RR* ) /\ ( A <_ A /\ A < w ) ) -> A <_ w )
17 16 ex 
 |-  ( ( A e. RR* /\ A e. RR* /\ w e. RR* ) -> ( ( A <_ A /\ A < w ) -> A <_ w ) )
18 9 10 11 9 12 17 ixxun 
 |-  ( ( ( A e. RR* /\ A e. RR* /\ B e. RR* ) /\ ( A <_ A /\ A <_ B ) ) -> ( ( A [,] A ) u. ( A (,] B ) ) = ( A [,] B ) )
19 4 4 5 7 8 18 syl32anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] A ) u. ( A (,] B ) ) = ( A [,] B ) )
20 3 19 eqtr3d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( { A } u. ( A (,] B ) ) = ( A [,] B ) )