Description: A consequence of relative atomicity. ( chrelat2i analog.) (Contributed by NM, 5-Feb-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlrelat2.b | |
|
hlrelat2.l | |
||
hlrelat2.a | |
||
Assertion | hlrelat2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlrelat2.b | |
|
2 | hlrelat2.l | |
|
3 | hlrelat2.a | |
|
4 | hllat | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 1 2 5 6 | latnlemlt | |
8 | 4 7 | syl3an1 | |
9 | simp1 | |
|
10 | 1 6 | latmcl | |
11 | 4 10 | syl3an1 | |
12 | simp2 | |
|
13 | eqid | |
|
14 | 1 2 5 13 3 | hlrelat | |
15 | 14 | ex | |
16 | 9 11 12 15 | syl3anc | |
17 | simpl1 | |
|
18 | 17 | hllatd | |
19 | 11 | adantr | |
20 | 1 3 | atbase | |
21 | 20 | adantl | |
22 | simpl2 | |
|
23 | 1 2 13 | latjle12 | |
24 | 18 19 21 22 23 | syl13anc | |
25 | simpr | |
|
26 | 24 25 | syl6bir | |
27 | 26 | adantld | |
28 | simpl3 | |
|
29 | 1 2 6 | latlem12 | |
30 | 18 21 22 28 29 | syl13anc | |
31 | 30 | notbid | |
32 | 1 2 5 13 | latnle | |
33 | 18 19 21 32 | syl3anc | |
34 | 31 33 | bitrd | |
35 | 34 24 | anbi12d | |
36 | pm3.21 | |
|
37 | orcom | |
|
38 | pm4.55 | |
|
39 | imor | |
|
40 | 37 38 39 | 3bitr4ri | |
41 | 36 40 | sylib | |
42 | 41 | con2i | |
43 | 42 | adantrl | |
44 | 35 43 | syl6bir | |
45 | 27 44 | jcad | |
46 | 45 | reximdva | |
47 | 16 46 | syld | |
48 | 8 47 | sylbid | |
49 | 1 2 | lattr | |
50 | 18 21 22 28 49 | syl13anc | |
51 | 50 | exp4b | |
52 | 51 | com34 | |
53 | 52 | com23 | |
54 | 53 | ralrimdv | |
55 | iman | |
|
56 | 55 | ralbii | |
57 | ralnex | |
|
58 | 56 57 | bitri | |
59 | 54 58 | syl6ib | |
60 | 59 | con2d | |
61 | 48 60 | impbid | |