Metamath Proof Explorer

Theorem snunioo1

Description: The closure of one end of an open real interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

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