# 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 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to \left({A},{B}\right)\cap \left({C},{D}\right)\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 simpll1 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to {A}\in {ℝ}^{*}$
2 simpll2 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to {B}\in {ℝ}^{*}$
3 simplr1 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to {C}\in {ℝ}^{*}$
4 simplr2 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to {D}\in {ℝ}^{*}$
5 iooin ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\right)\right)\to \left({A},{B}\right)\cap \left({C},{D}\right)=\left(if\left({A}\le {C},{C},{A}\right),if\left({B}\le {D},{B},{D}\right)\right)$
6 1 2 3 4 5 syl22anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to \left({A},{B}\right)\cap \left({C},{D}\right)=\left(if\left({A}\le {C},{C},{A}\right),if\left({B}\le {D},{B},{D}\right)\right)$
7 simprr ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to {D}\le {B}$
8 xrmineq ${⊢}\left({B}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {D}\le {B}\right)\to if\left({B}\le {D},{B},{D}\right)={D}$
9 2 4 7 8 syl3anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to if\left({B}\le {D},{B},{D}\right)={D}$
10 9 oveq2d ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to \left(if\left({A}\le {C},{C},{A}\right),if\left({B}\le {D},{B},{D}\right)\right)=\left(if\left({A}\le {C},{C},{A}\right),{D}\right)$
11 simpr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge {A}\le {C}\right)\to {A}\le {C}$
12 11 iftrued ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge {A}\le {C}\right)\to if\left({A}\le {C},{C},{A}\right)={C}$
13 simplr3 ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to {C}<{D}$
14 13 adantr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge {A}\le {C}\right)\to {C}<{D}$
15 12 14 eqbrtrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge {A}\le {C}\right)\to if\left({A}\le {C},{C},{A}\right)<{D}$
16 simpr ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge ¬{A}\le {C}\right)\to ¬{A}\le {C}$
17 16 iffalsed ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge ¬{A}\le {C}\right)\to if\left({A}\le {C},{C},{A}\right)={A}$
18 simplrl ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge ¬{A}\le {C}\right)\to {A}<{D}$
19 17 18 eqbrtrd ${⊢}\left(\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\wedge ¬{A}\le {C}\right)\to if\left({A}\le {C},{C},{A}\right)<{D}$
20 15 19 pm2.61dan ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to if\left({A}\le {C},{C},{A}\right)<{D}$
21 3 1 ifcld ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to if\left({A}\le {C},{C},{A}\right)\in {ℝ}^{*}$
22 ioon0 ${⊢}\left(if\left({A}\le {C},{C},{A}\right)\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\right)\to \left(\left(if\left({A}\le {C},{C},{A}\right),{D}\right)\ne \varnothing ↔if\left({A}\le {C},{C},{A}\right)<{D}\right)$
23 21 4 22 syl2anc ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to \left(\left(if\left({A}\le {C},{C},{A}\right),{D}\right)\ne \varnothing ↔if\left({A}\le {C},{C},{A}\right)<{D}\right)$
24 20 23 mpbird ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to \left(if\left({A}\le {C},{C},{A}\right),{D}\right)\ne \varnothing$
25 10 24 eqnetrd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to \left(if\left({A}\le {C},{C},{A}\right),if\left({B}\le {D},{B},{D}\right)\right)\ne \varnothing$
26 6 25 eqnetrd ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {A}<{B}\right)\wedge \left({C}\in {ℝ}^{*}\wedge {D}\in {ℝ}^{*}\wedge {C}<{D}\right)\right)\wedge \left({A}<{D}\wedge {D}\le {B}\right)\right)\to \left({A},{B}\right)\cap \left({C},{D}\right)\ne \varnothing$