Description: The union of two adjacent left-closed right-open real intervals is a left-closed right-open real interval. (Contributed by Paul Chapman, 15-Mar-2008) (Proof shortened by Mario Carneiro, 16-Jun-2014)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | icoun | |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,) B ) u. ( B [,) C ) ) = ( A [,) C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ico | |- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } ) |
|
| 2 | xrlenlt | |- ( ( B e. RR* /\ w e. RR* ) -> ( B <_ w <-> -. w < B ) ) |
|
| 3 | xrltletr | |- ( ( w e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w < B /\ B <_ C ) -> w < C ) ) |
|
| 4 | xrletr | |- ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A <_ B /\ B <_ w ) -> A <_ w ) ) |
|
| 5 | 1 1 2 1 3 4 | ixxun | |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A <_ B /\ B <_ C ) ) -> ( ( A [,) B ) u. ( B [,) C ) ) = ( A [,) C ) ) |