Metamath Proof Explorer

Theorem eliccioo

Description: Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016)

Ref Expression
Assertion eliccioo 
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( C e. ( A [,] B ) <-> ( C = A \/ C e. ( A (,) B ) \/ C = 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 eleq2d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( C e. ( ( A (,) B ) u. { A , B } ) <-> C e. ( A [,] B ) ) )
3 2 biimpar 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C e. ( A [,] B ) ) -> C e. ( ( A (,) B ) u. { A , B } ) )
4 elun 
 |-  ( C e. ( ( A (,) B ) u. { A , B } ) <-> ( C e. ( A (,) B ) \/ C e. { A , B } ) )
5 elprg 
 |-  ( C e. ( A [,] B ) -> ( C e. { A , B } <-> ( C = A \/ C = B ) ) )
6 5 orbi2d 
 |-  ( C e. ( A [,] B ) -> ( ( C e. ( A (,) B ) \/ C e. { A , B } ) <-> ( C e. ( A (,) B ) \/ ( C = A \/ C = B ) ) ) )
7 4 6 syl5bb 
 |-  ( C e. ( A [,] B ) -> ( C e. ( ( A (,) B ) u. { A , B } ) <-> ( C e. ( A (,) B ) \/ ( C = A \/ C = B ) ) ) )
8 7 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C e. ( A [,] B ) ) -> ( C e. ( ( A (,) B ) u. { A , B } ) <-> ( C e. ( A (,) B ) \/ ( C = A \/ C = B ) ) ) )
9 3 8 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C e. ( A [,] B ) ) -> ( C e. ( A (,) B ) \/ ( C = A \/ C = B ) ) )
10 3orass 
 |-  ( ( C e. ( A (,) B ) \/ C = A \/ C = B ) <-> ( C e. ( A (,) B ) \/ ( C = A \/ C = B ) ) )
11 3orcoma 
 |-  ( ( C e. ( A (,) B ) \/ C = A \/ C = B ) <-> ( C = A \/ C e. ( A (,) B ) \/ C = B ) )
12 10 11 bitr3i 
 |-  ( ( C e. ( A (,) B ) \/ ( C = A \/ C = B ) ) <-> ( C = A \/ C e. ( A (,) B ) \/ C = B ) )
13 9 12 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C e. ( A [,] B ) ) -> ( C = A \/ C e. ( A (,) B ) \/ C = B ) )
14 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
15 14 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = A ) -> A e. ( A [,] B ) )
16 eleq1 
 |-  ( C = A -> ( C e. ( A [,] B ) <-> A e. ( A [,] B ) ) )
17 16 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = A ) -> ( C e. ( A [,] B ) <-> A e. ( A [,] B ) ) )
18 15 17 mpbird 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = A ) -> C e. ( A [,] B ) )
19 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
20 19 sseli 
 |-  ( C e. ( A (,) B ) -> C e. ( A [,] B ) )
21 20 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C e. ( A (,) B ) ) -> C e. ( A [,] B ) )
22 ubicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. ( A [,] B ) )
23 22 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> B e. ( A [,] B ) )
24 eleq1 
 |-  ( C = B -> ( C e. ( A [,] B ) <-> B e. ( A [,] B ) ) )
25 24 adantl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> ( C e. ( A [,] B ) <-> B e. ( A [,] B ) ) )
26 23 25 mpbird 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ C = B ) -> C e. ( A [,] B ) )
27 18 21 26 3jaodan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A <_ B ) /\ ( C = A \/ C e. ( A (,) B ) \/ C = B ) ) -> C e. ( A [,] B ) )
28 13 27 impbida 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( C e. ( A [,] B ) <-> ( C = A \/ C e. ( A (,) B ) \/ C = B ) ) )