Description: An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of Kalmbach p. 149. (Contributed by NM, 21-Oct-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlrelat5.b | |
|
hlrelat5.l | |
||
hlrelat5.s | |
||
hlrelat5.j | |
||
hlrelat5.a | |
||
Assertion | hlrelat5N | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlrelat5.b | |
|
2 | hlrelat5.l | |
|
3 | hlrelat5.s | |
|
4 | hlrelat5.j | |
|
5 | hlrelat5.a | |
|
6 | 1 2 3 5 | hlrelat1 | |
7 | 6 | imp | |
8 | hllat | |
|
9 | id | |
|
10 | 1 5 | atbase | |
11 | ovexd | |
|
12 | 2 3 | pltval | |
13 | 11 12 | syl3an3 | |
14 | 1 2 4 | latlej1 | |
15 | 14 | biantrurd | |
16 | 13 15 | bitr4d | |
17 | 1 2 4 | latleeqj1 | |
18 | 17 | 3com23 | |
19 | 1 4 | latjcom | |
20 | 19 | eqeq1d | |
21 | 18 20 | bitr4d | |
22 | 21 | notbid | |
23 | nesym | |
|
24 | 22 23 | bitr4di | |
25 | 16 24 | bitr4d | |
26 | 8 9 10 25 | syl3an | |
27 | 26 | 3expa | |
28 | 27 | anbi1d | |
29 | 28 | rexbidva | |
30 | 29 | 3adant3 | |
31 | 30 | adantr | |
32 | 7 31 | mpbird | |