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 ) ) =/= (/) )