Description: Idempotence of join operation. Frequently-used special case of latjcom for atoms. (Contributed by NM, 15-Jul-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | hlatjcom.j | |
|
hlatjcom.a | |
||
Assertion | hlatjidm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlatjcom.j | |
|
2 | hlatjcom.a | |
|
3 | hllat | |
|
4 | eqid | |
|
5 | 4 2 | atbase | |
6 | 4 1 | latjidm | |
7 | 3 5 6 | syl2an | |