Theorem iccdifioo

Description: If the open inverval is removed from the closed interval, only the bounds are left. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		prunioo	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A (,) B ) u. { A , B } ) = ( A [,] B ) )
2		uncom	|- ( ( A (,) B ) u. { A , B } ) = ( { A , B } u. ( A (,) B ) )
3	1 2	eqtr3di	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A [,] B ) = ( { A , B } u. ( A (,) B ) ) )
4	3	difeq1d	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = ( ( { A , B } u. ( A (,) B ) ) \ ( A (,) B ) ) )
5		difun2	|- ( ( { A , B } u. ( A (,) B ) ) \ ( A (,) B ) ) = ( { A , B } \ ( A (,) B ) )
6	5	a1i	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( { A , B } u. ( A (,) B ) ) \ ( A (,) B ) ) = ( { A , B } \ ( A (,) B ) ) )
7		incom	|- ( ( A (,) B ) i^i { A , B } ) = ( { A , B } i^i ( A (,) B ) )
8		iooinlbub	|- ( ( A (,) B ) i^i { A , B } ) = (/)
9	7 8	eqtr3i	|- ( { A , B } i^i ( A (,) B ) ) = (/)
10		disj3	|- ( ( { A , B } i^i ( A (,) B ) ) = (/) <-> { A , B } = ( { A , B } \ ( A (,) B ) ) )
11	9 10	mpbi	|- { A , B } = ( { A , B } \ ( A (,) B ) )
12	11	eqcomi	|- ( { A , B } \ ( A (,) B ) ) = { A , B }
13	12	a1i	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( { A , B } \ ( A (,) B ) ) = { A , B } )
14	4 6 13	3eqtrd	|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] B ) \ ( A (,) B ) ) = { A , B } )