Metamath Proof Explorer

Theorem iccdifprioo

Description: An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion iccdifprioo 
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( 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 1 eqcomd 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A [,] B ) = ( ( A (,) B ) u. { A , B } ) )
3 2 difeq1d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] B ) \ { A , B } ) = ( ( ( A (,) B ) u. { A , B } ) \ { A , B } ) )
4 difun2 
 |-  ( ( ( A (,) B ) u. { A , B } ) \ { A , B } ) = ( ( A (,) B ) \ { A , B } )
5 iooinlbub 
 |-  ( ( A (,) B ) i^i { A , B } ) = (/)
6 disj3 
 |-  ( ( ( A (,) B ) i^i { A , B } ) = (/) <-> ( A (,) B ) = ( ( A (,) B ) \ { A , B } ) )
7 5 6 mpbi 
 |-  ( A (,) B ) = ( ( A (,) B ) \ { A , B } )
8 4 7 eqtr4i 
 |-  ( ( ( A (,) B ) u. { A , B } ) \ { A , B } ) = ( A (,) B )
9 3 8 eqtrdi 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( ( A [,] B ) \ { A , B } ) = ( A (,) B ) )
10 9 3expa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ A <_ B ) -> ( ( A [,] B ) \ { A , B } ) = ( A (,) B ) )
11 difssd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( ( A [,] B ) \ { A , B } ) C_ ( A [,] B ) )
12 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> -. A <_ B )
13 xrlenlt 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
14 13 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( A <_ B <-> -. B < A ) )
15 12 14 mtbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> -. -. B < A )
16 15 notnotrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> B < A )
17 icc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
18 17 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( ( A [,] B ) = (/) <-> B < A ) )
19 16 18 mpbird 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( A [,] B ) = (/) )
20 11 19 sseqtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( ( A [,] B ) \ { A , B } ) C_ (/) )
21 ss0 
 |-  ( ( ( A [,] B ) \ { A , B } ) C_ (/) -> ( ( A [,] B ) \ { A , B } ) = (/) )
22 20 21 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( ( A [,] B ) \ { A , B } ) = (/) )
23 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> B e. RR* )
24 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> A e. RR* )
25 23 24 16 xrltled 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> B <_ A )
26 ioo0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
27 26 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )
28 25 27 mpbird 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( A (,) B ) = (/) )
29 22 28 eqtr4d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. A <_ B ) -> ( ( A [,] B ) \ { A , B } ) = ( A (,) B ) )
30 10 29 pm2.61dan 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) \ { A , B } ) = ( A (,) B ) )