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∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→AB∩CD≠∅

Proof

Step Hyp Ref Expression
1 simpll1 ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→A∈ℝ*
2 simpll2 ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→B∈ℝ*
3 simplr1 ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→C∈ℝ*
4 simplr2 ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→D∈ℝ*
5 iooin ⊢A∈ℝ*∧B∈ℝ*∧C∈ℝ*∧D∈ℝ*→AB∩CD=ifA≤CCAifB≤DBD
6 1 2 3 4 5 syl22anc ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→AB∩CD=ifA≤CCAifB≤DBD
7 simprl ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→A≤C
8 7 iftrued ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→ifA≤CCA=C
9 8 oveq1d ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→ifA≤CCAifB≤DBD=CifB≤DBD
10 simprr ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→C<B
11 simplr3 ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→C<D
12 10 11 jca ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→C<B∧C<D
13 xrltmin ⊢C∈ℝ*∧B∈ℝ*∧D∈ℝ*→C<ifB≤DBD↔C<B∧C<D
14 3 2 4 13 syl3anc ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→C<ifB≤DBD↔C<B∧C<D
15 12 14 mpbird ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→C<ifB≤DBD
16 2 4 ifcld ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→ifB≤DBD∈ℝ*
17 ioon0 ⊢C∈ℝ*∧ifB≤DBD∈ℝ*→CifB≤DBD≠∅↔C<ifB≤DBD
18 3 16 17 syl2anc ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→CifB≤DBD≠∅↔C<ifB≤DBD
19 15 18 mpbird ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→CifB≤DBD≠∅
20 9 19 eqnetrd ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→ifA≤CCAifB≤DBD≠∅
21 6 20 eqnetrd ⊢A∈ℝ*∧B∈ℝ*∧A<B∧C∈ℝ*∧D∈ℝ*∧C<D∧A≤C∧C<B→AB∩CD≠∅