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