Metamath Proof Explorer


Theorem ioondisj1

Description: A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step Hyp Ref Expression
1 simpll1
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> A e. RR* )
2 simpll2
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> B e. RR* )
3 simplr1
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C e. RR* )
4 simplr2
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> D e. RR* )
5 iooin
 |-  ( ( ( 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 ) ) )
6 1 2 3 4 5 syl22anc
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) )
7 simprl
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> A <_ C )
8 7 iftrued
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> if ( A <_ C , C , A ) = C )
9 8 oveq1d
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) = ( C (,) if ( B <_ D , B , D ) ) )
10 simprr
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C < B )
11 simplr3
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C < D )
12 10 11 jca
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( C < B /\ C < D ) )
13 xrltmin
 |-  ( ( C e. RR* /\ B e. RR* /\ D e. RR* ) -> ( C < if ( B <_ D , B , D ) <-> ( C < B /\ C < D ) ) )
14 3 2 4 13 syl3anc
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( C < if ( B <_ D , B , D ) <-> ( C < B /\ C < D ) ) )
15 12 14 mpbird
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> C < if ( B <_ D , B , D ) )
16 2 4 ifcld
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> if ( B <_ D , B , D ) e. RR* )
17 ioon0
 |-  ( ( C e. RR* /\ if ( B <_ D , B , D ) e. RR* ) -> ( ( C (,) if ( B <_ D , B , D ) ) =/= (/) <-> C < if ( B <_ D , B , D ) ) )
18 3 16 17 syl2anc
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( ( C (,) if ( B <_ D , B , D ) ) =/= (/) <-> C < if ( B <_ D , B , D ) ) )
19 15 18 mpbird
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( C (,) if ( B <_ D , B , D ) ) =/= (/) )
20 9 19 eqnetrd
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) =/= (/) )
21 6 20 eqnetrd
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A <_ C /\ C < B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) =/= (/) )