This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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