Metamath Proof Explorer

Theorem icoiccdif

Description: Left-closed right-open interval gotten by a closed iterval taking away the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 icossicc 
 |-  ( A [,) B ) C_ ( A [,] B )
2 1 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) C_ ( A [,] B ) )
3 2 sselda 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> x e. ( A [,] B ) )
4 elico1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,) B ) <-> ( x e. RR* /\ A <_ x /\ x < B ) ) )
5 4 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> ( x e. RR* /\ A <_ x /\ x < B ) )
6 5 simp1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> x e. RR* )
7 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> B e. RR* )
8 5 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> x < B )
9 xrltne 
 |-  ( ( x e. RR* /\ B e. RR* /\ x < B ) -> B =/= x )
10 6 7 8 9 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> B =/= x )
11 10 necomd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> x =/= B )
12 11 neneqd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> -. x = B )
13 velsn 
 |-  ( x e. { B } <-> x = B )
14 12 13 sylnibr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> -. x e. { B } )
15 3 14 eldifd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( A [,) B ) ) -> x e. ( ( A [,] B ) \ { B } ) )
16 15 ex 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,) B ) -> x e. ( ( A [,] B ) \ { B } ) ) )
17 16 ssrdv 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) C_ ( ( A [,] B ) \ { B } ) )
18 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> A e. RR* )
19 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> B e. RR* )
20 eldifi 
 |-  ( x e. ( ( A [,] B ) \ { B } ) -> x e. ( A [,] B ) )
21 eliccxr 
 |-  ( x e. ( A [,] B ) -> x e. RR* )
22 20 21 syl 
 |-  ( x e. ( ( A [,] B ) \ { B } ) -> x e. RR* )
23 22 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> x e. RR* )
24 20 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> x e. ( A [,] B ) )
25 elicc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ x /\ x <_ B ) ) )
26 25 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> ( x e. ( A [,] B ) <-> ( x e. RR* /\ A <_ x /\ x <_ B ) ) )
27 24 26 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> ( x e. RR* /\ A <_ x /\ x <_ B ) )
28 27 simp2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> A <_ x )
29 eldifsni 
 |-  ( x e. ( ( A [,] B ) \ { B } ) -> x =/= B )
30 29 necomd 
 |-  ( x e. ( ( A [,] B ) \ { B } ) -> B =/= x )
31 30 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> B =/= x )
32 27 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> x <_ B )
33 xrleltne 
 |-  ( ( x e. RR* /\ B e. RR* /\ x <_ B ) -> ( x < B <-> B =/= x ) )
34 23 19 32 33 syl3anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> ( x < B <-> B =/= x ) )
35 31 34 mpbird 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> x < B )
36 18 19 23 28 35 elicod 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. ( ( A [,] B ) \ { B } ) ) -> x e. ( A [,) B ) )
37 17 36 eqelssd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = ( ( A [,] B ) \ { B } ) )