This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iocioodisjd

Description: Adjacent intervals where the lower interval is right-closed and the upper interval is open are disjoint. (Contributed by SN, 1-Oct-2025)

Ref Expression
Hypotheses ixxdisjd.a 
|- ( ph -> A e. RR* )
ixxdisjd.b 
|- ( ph -> B e. RR* )
ixxdisjd.c 
|- ( ph -> C e. RR* )
Assertion iocioodisjd 
|- ( ph -> ( ( A (,] B ) i^i ( B (,) C ) ) = (/) )

Proof

Step Hyp Ref Expression
1 ixxdisjd.a 
 |-  ( ph -> A e. RR* )
2 ixxdisjd.b 
 |-  ( ph -> B e. RR* )
3 ixxdisjd.c 
 |-  ( ph -> C e. RR* )
4 df-ioc 
 |-  (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
5 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
6 xrltnle 
 |-  ( ( B e. RR* /\ w e. RR* ) -> ( B < w <-> -. w <_ B ) )
7 4 5 6 ixxdisj 
 |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A (,] B ) i^i ( B (,) C ) ) = (/) )
8 1 2 3 7 syl3anc 
 |-  ( ph -> ( ( A (,] B ) i^i ( B (,) C ) ) = (/) )