Description: Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | eliccelico | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl1 | |
|
2 | simpl2 | |
|
3 | simprl | |
|
4 | elicc1 | |
|
5 | 4 | biimpa | |
6 | 5 | simp1d | |
7 | 1 2 3 6 | syl21anc | |
8 | 5 | simp3d | |
9 | 1 2 3 8 | syl21anc | |
10 | 1 2 | jca | |
11 | simprr | |
|
12 | 5 | simp2d | |
13 | 10 3 12 | syl2anc | |
14 | elico1 | |
|
15 | 14 | notbid | |
16 | 15 | biimpa | |
17 | df-3an | |
|
18 | 17 | notbii | |
19 | imnan | |
|
20 | 18 19 | bitr4i | |
21 | 16 20 | sylib | |
22 | 21 | imp | |
23 | 10 11 7 13 22 | syl22anc | |
24 | xeqlelt | |
|
25 | 24 | biimpar | |
26 | 7 2 9 23 25 | syl22anc | |
27 | 26 | ex | |
28 | pm5.6 | |
|
29 | 27 28 | sylib | |
30 | icossicc | |
|
31 | simpr | |
|
32 | 30 31 | sselid | |
33 | simpr | |
|
34 | simpl2 | |
|
35 | 33 34 | eqeltrd | |
36 | simpl3 | |
|
37 | 36 33 | breqtrrd | |
38 | 34 | xrleidd | |
39 | 33 38 | eqbrtrd | |
40 | simpl1 | |
|
41 | 40 34 4 | syl2anc | |
42 | 35 37 39 41 | mpbir3and | |
43 | 32 42 | jaodan | |
44 | 43 | ex | |
45 | 29 44 | impbid | |