Description: A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | ioondisj1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll1 | |
|
2 | simpll2 | |
|
3 | simplr1 | |
|
4 | simplr2 | |
|
5 | iooin | |
|
6 | 1 2 3 4 5 | syl22anc | |
7 | simprl | |
|
8 | 7 | iftrued | |
9 | 8 | oveq1d | |
10 | simprr | |
|
11 | simplr3 | |
|
12 | 10 11 | jca | |
13 | xrltmin | |
|
14 | 3 2 4 13 | syl3anc | |
15 | 12 14 | mpbird | |
16 | 2 4 | ifcld | |
17 | ioon0 | |
|
18 | 3 16 17 | syl2anc | |
19 | 15 18 | mpbird | |
20 | 9 19 | eqnetrd | |
21 | 6 20 | eqnetrd | |