Metamath Proof Explorer

Theorem elioc2

Description: Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007) (Revised by Mario Carneiro, 14-Jun-2014)

Ref Expression
Assertion elioc2 
|- ( ( A e. RR* /\ B e. RR ) -> ( C e. ( A (,] B ) <-> ( C e. RR /\ A < C /\ C <_ B ) ) )

Proof

Step Hyp Ref Expression
1 rexr 
 |-  ( B e. RR -> B e. RR* )
2 elioc1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) )
3 1 2 sylan2 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) )
4 mnfxr 
 |-  -oo e. RR*
5 4 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> -oo e. RR* )
6 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> A e. RR* )
7 simpr1 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> C e. RR* )
8 mnfle 
 |-  ( A e. RR* -> -oo <_ A )
9 8 ad2antrr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> -oo <_ A )
10 simpr2 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> A < C )
11 5 6 7 9 10 xrlelttrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> -oo < C )
12 1 ad2antlr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> B e. RR* )
13 pnfxr 
 |-  +oo e. RR*
14 13 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> +oo e. RR* )
15 simpr3 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> C <_ B )
16 ltpnf 
 |-  ( B e. RR -> B < +oo )
17 16 ad2antlr 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> B < +oo )
18 7 12 14 15 17 xrlelttrd 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> C < +oo )
19 xrrebnd 
 |-  ( C e. RR* -> ( C e. RR <-> ( -oo < C /\ C < +oo ) ) )
20 7 19 syl 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> ( C e. RR <-> ( -oo < C /\ C < +oo ) ) )
21 11 18 20 mpbir2and 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> C e. RR )
22 21 10 15 3jca 
 |-  ( ( ( A e. RR* /\ B e. RR ) /\ ( C e. RR* /\ A < C /\ C <_ B ) ) -> ( C e. RR /\ A < C /\ C <_ B ) )
23 22 ex 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( C e. RR* /\ A < C /\ C <_ B ) -> ( C e. RR /\ A < C /\ C <_ B ) ) )
24 rexr 
 |-  ( C e. RR -> C e. RR* )
25 24 3anim1i 
 |-  ( ( C e. RR /\ A < C /\ C <_ B ) -> ( C e. RR* /\ A < C /\ C <_ B ) )
26 23 25 impbid1 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( ( C e. RR* /\ A < C /\ C <_ B ) <-> ( C e. RR /\ A < C /\ C <_ B ) ) )
27 3 26 bitrd 
 |-  ( ( A e. RR* /\ B e. RR ) -> ( C e. ( A (,] B ) <-> ( C e. RR /\ A < C /\ C <_ B ) ) )