Metamath Proof Explorer


Theorem iccdisj2

Description: If the upper bound of one closed interval is less than the lower bound of the other, the intervals are disjoint. (Contributed by Zhi Wang, 9-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> A e. RR* )
2 simp3
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> B < C )
3 ltrelxr
 |-  < C_ ( RR* X. RR* )
4 3 brel
 |-  ( B < C -> ( B e. RR* /\ C e. RR* ) )
5 2 4 syl
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( B e. RR* /\ C e. RR* ) )
6 5 simprd
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> C e. RR* )
7 1 xrleidd
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> A <_ A )
8 iccssico
 |-  ( ( ( A e. RR* /\ C e. RR* ) /\ ( A <_ A /\ B < C ) ) -> ( A [,] B ) C_ ( A [,) C ) )
9 1 6 7 2 8 syl22anc
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( A [,] B ) C_ ( A [,) C ) )
10 simp2
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> D e. RR* )
11 df-ico
 |-  [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
12 df-icc
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
13 xrlenlt
 |-  ( ( C e. RR* /\ w e. RR* ) -> ( C <_ w <-> -. w < C ) )
14 11 12 13 ixxdisj
 |-  ( ( A e. RR* /\ C e. RR* /\ D e. RR* ) -> ( ( A [,) C ) i^i ( C [,] D ) ) = (/) )
15 1 6 10 14 syl3anc
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( ( A [,) C ) i^i ( C [,] D ) ) = (/) )
16 9 15 ssdisjd
 |-  ( ( A e. RR* /\ D e. RR* /\ B < C ) -> ( ( A [,] B ) i^i ( C [,] D ) ) = (/) )