Metamath Proof Explorer

Theorem elicc2

Description: Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007) (Revised by Mario Carneiro, 14-Jun-2014)

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

Proof

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