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

Metamath Proof Explorer

Theorem ioondisj2

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

Ref Expression
Assertion ioondisj2 
|- ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ 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 < D /\ D <_ B ) ) -> A e. RR* )
2 simpll2 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> B e. RR* )
3 simplr1 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> C e. RR* )
4 simplr2 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ 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 < D /\ D <_ B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) = ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) )
7 simprr 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> D <_ B )
8 xrmineq 
 |-  ( ( B e. RR* /\ D e. RR* /\ D <_ B ) -> if ( B <_ D , B , D ) = D )
9 2 4 7 8 syl3anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> if ( B <_ D , B , D ) = D )
10 9 oveq2d 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) = ( if ( A <_ C , C , A ) (,) D ) )
11 simpr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ A <_ C ) -> A <_ C )
12 11 iftrued 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ A <_ C ) -> if ( A <_ C , C , A ) = C )
13 simplr3 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> C < D )
14 13 adantr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ A <_ C ) -> C < D )
15 12 14 eqbrtrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ A <_ C ) -> if ( A <_ C , C , A ) < D )
16 simpr 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ -. A <_ C ) -> -. A <_ C )
17 16 iffalsed 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ -. A <_ C ) -> if ( A <_ C , C , A ) = A )
18 simplrl 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ -. A <_ C ) -> A < D )
19 17 18 eqbrtrd 
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) /\ -. A <_ C ) -> if ( A <_ C , C , A ) < D )
20 15 19 pm2.61dan 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> if ( A <_ C , C , A ) < D )
21 3 1 ifcld 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> if ( A <_ C , C , A ) e. RR* )
22 ioon0 
 |-  ( ( if ( A <_ C , C , A ) e. RR* /\ D e. RR* ) -> ( ( if ( A <_ C , C , A ) (,) D ) =/= (/) <-> if ( A <_ C , C , A ) < D ) )
23 21 4 22 syl2anc 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> ( ( if ( A <_ C , C , A ) (,) D ) =/= (/) <-> if ( A <_ C , C , A ) < D ) )
24 20 23 mpbird 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> ( if ( A <_ C , C , A ) (,) D ) =/= (/) )
25 10 24 eqnetrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> ( if ( A <_ C , C , A ) (,) if ( B <_ D , B , D ) ) =/= (/) )
26 6 25 eqnetrd 
 |-  ( ( ( ( A e. RR* /\ B e. RR* /\ A < B ) /\ ( C e. RR* /\ D e. RR* /\ C < D ) ) /\ ( A < D /\ D <_ B ) ) -> ( ( A (,) B ) i^i ( C (,) D ) ) =/= (/) )