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 ) )