Theorem iccin

Description: Intersection of two closed intervals of extended reals. (Contributed by Zhi Wang, 9-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-icc	|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
2		xrmaxle	|- ( ( A e. RR* /\ C e. RR* /\ z e. RR* ) -> ( if ( A <_ C , C , A ) <_ z <-> ( A <_ z /\ C <_ z ) ) )
3		xrlemin	|- ( ( z e. RR* /\ B e. RR* /\ D e. RR* ) -> ( z <_ if ( B <_ D , B , D ) <-> ( z <_ B /\ z <_ D ) ) )
4	1 2 3	ixxin	|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A [,] B ) i^i ( C [,] D ) ) = ( if ( A <_ C , C , A ) [,] if ( B <_ D , B , D ) ) )