Metamath Proof Explorer

Theorem elicoelioo

Description: Relate elementhood to a closed-below, open-above interval with elementhood to the same open interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Assertion elicoelioo 
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( C e. ( A [,) B ) <-> ( C = A \/ C e. ( A (,) B ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> A e. RR* )
2 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> B e. RR* )
3 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> C e. ( A [,) B ) )
4 elico1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,) B ) <-> ( C e. RR* /\ A <_ C /\ C < B ) ) )
5 4 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,) B ) ) -> ( C e. RR* /\ A <_ C /\ C < B ) )
6 5 simp1d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,) B ) ) -> C e. RR* )
7 1 2 3 6 syl21anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> C e. RR* )
8 5 simp2d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,) B ) ) -> A <_ C )
9 1 2 3 8 syl21anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> A <_ C )
10 1 2 jca 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> ( A e. RR* /\ B e. RR* ) )
11 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> -. C e. ( A (,) B ) )
12 5 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ C e. ( A [,) B ) ) -> C < B )
13 10 3 12 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> C < B )
14 elioo1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR* /\ A < C /\ C < B ) ) )
15 14 notbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. C e. ( A (,) B ) <-> -. ( C e. RR* /\ A < C /\ C < B ) ) )
16 15 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. C e. ( A (,) B ) ) -> -. ( C e. RR* /\ A < C /\ C < B ) )
17 3anan32 
 |-  ( ( C e. RR* /\ A < C /\ C < B ) <-> ( ( C e. RR* /\ C < B ) /\ A < C ) )
18 17 notbii 
 |-  ( -. ( C e. RR* /\ A < C /\ C < B ) <-> -. ( ( C e. RR* /\ C < B ) /\ A < C ) )
19 imnan 
 |-  ( ( ( C e. RR* /\ C < B ) -> -. A < C ) <-> -. ( ( C e. RR* /\ C < B ) /\ A < C ) )
20 18 19 bitr4i 
 |-  ( -. ( C e. RR* /\ A < C /\ C < B ) <-> ( ( C e. RR* /\ C < B ) -> -. A < C ) )
21 16 20 sylib 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. C e. ( A (,) B ) ) -> ( ( C e. RR* /\ C < B ) -> -. A < C ) )
22 21 imp 
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. C e. ( A (,) B ) ) /\ ( C e. RR* /\ C < B ) ) -> -. A < C )
23 10 11 7 13 22 syl22anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> -. A < C )
24 xeqlelt 
 |-  ( ( A e. RR* /\ C e. RR* ) -> ( A = C <-> ( A <_ C /\ -. A < C ) ) )
25 24 biimpar 
 |-  ( ( ( A e. RR* /\ C e. RR* ) /\ ( A <_ C /\ -. A < C ) ) -> A = C )
26 1 7 9 23 25 syl22anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) ) -> A = C )
27 26 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) -> A = C ) )
28 eqcom 
 |-  ( A = C <-> C = A )
29 27 28 syl6ib 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) -> C = A ) )
30 pm5.6 
 |-  ( ( ( C e. ( A [,) B ) /\ -. C e. ( A (,) B ) ) -> C = A ) <-> ( C e. ( A [,) B ) -> ( C e. ( A (,) B ) \/ C = A ) ) )
31 29 30 sylib 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( C e. ( A [,) B ) -> ( C e. ( A (,) B ) \/ C = A ) ) )
32 orcom 
 |-  ( ( C e. ( A (,) B ) \/ C = A ) <-> ( C = A \/ C e. ( A (,) B ) ) )
33 31 32 syl6ib 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( C e. ( A [,) B ) -> ( C = A \/ C e. ( A (,) B ) ) ) )
34 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> C = A )
35 simpl1 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> A e. RR* )
36 34 35 eqeltrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> C e. RR* )
37 35 xrleidd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> A <_ A )
38 37 34 breqtrrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> A <_ C )
39 simpl3 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> A < B )
40 34 39 eqbrtrd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> C < B )
41 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> B e. RR* )
42 35 41 4 syl2anc 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> ( C e. ( A [,) B ) <-> ( C e. RR* /\ A <_ C /\ C < B ) ) )
43 36 38 40 42 mpbir3and 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C = A ) -> C e. ( A [,) B ) )
44 ioossico 
 |-  ( A (,) B ) C_ ( A [,) B )
45 simpr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C e. ( A (,) B ) ) -> C e. ( A (,) B ) )
46 44 45 sseldi 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ C e. ( A (,) B ) ) -> C e. ( A [,) B ) )
47 43 46 jaodan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C = A \/ C e. ( A (,) B ) ) ) -> C e. ( A [,) B ) )
48 47 ex 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( C = A \/ C e. ( A (,) B ) ) -> C e. ( A [,) B ) ) )
49 33 48 impbid 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( C e. ( A [,) B ) <-> ( C = A \/ C e. ( A (,) B ) ) ) )