Metamath Proof Explorer

Theorem icodisj

Description: Adjacent left-closed right-open real intervals are disjoint. (Contributed by Mario Carneiro, 16-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( x e. ( ( A [,) B ) i^i ( B [,) C ) ) <-> ( x e. ( A [,) B ) /\ x e. ( B [,) C ) ) )
2 elico1 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( x e. ( A [,) B ) <-> ( x e. RR* /\ A <_ x /\ x < B ) ) )
3 2 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( A [,) B ) <-> ( x e. RR* /\ A <_ x /\ x < B ) ) )
4 3 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( A [,) B ) ) -> ( x e. RR* /\ A <_ x /\ x < B ) )
5 4 simp3d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( A [,) B ) ) -> x < B )
6 5 adantrr 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. ( A [,) B ) /\ x e. ( B [,) C ) ) ) -> x < B )
7 elico1 
 |-  ( ( B e. RR* /\ C e. RR* ) -> ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) ) )
8 7 3adant1 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) ) )
9 8 biimpa 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( B [,) C ) ) -> ( x e. RR* /\ B <_ x /\ x < C ) )
10 9 simp2d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( B [,) C ) ) -> B <_ x )
11 simpl2 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( B [,) C ) ) -> B e. RR* )
12 9 simp1d 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( B [,) C ) ) -> x e. RR* )
13 11 12 xrlenltd 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( B [,) C ) ) -> ( B <_ x <-> -. x < B ) )
14 10 13 mpbid 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ x e. ( B [,) C ) ) -> -. x < B )
15 14 adantrl 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( x e. ( A [,) B ) /\ x e. ( B [,) C ) ) ) -> -. x < B )
16 6 15 pm2.65da 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> -. ( x e. ( A [,) B ) /\ x e. ( B [,) C ) ) )
17 16 pm2.21d 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( x e. ( A [,) B ) /\ x e. ( B [,) C ) ) -> x e. (/) ) )
18 1 17 syl5bi 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( x e. ( ( A [,) B ) i^i ( B [,) C ) ) -> x e. (/) ) )
19 18 ssrdv 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A [,) B ) i^i ( B [,) C ) ) C_ (/) )
20 ss0 
 |-  ( ( ( A [,) B ) i^i ( B [,) C ) ) C_ (/) -> ( ( A [,) B ) i^i ( B [,) C ) ) = (/) )
21 19 20 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A [,) B ) i^i ( B [,) C ) ) = (/) )