Metamath Proof Explorer


Theorem hlatjcl

Description: Closure of join operation. Frequently-used special case of latjcl for atoms. (Contributed by NM, 15-Jun-2012)

Ref Expression
Hypotheses hlatjcl.b B = Base K
hlatjcl.j ˙ = join K
hlatjcl.a A = Atoms K
Assertion hlatjcl K HL X A Y A X ˙ Y B

Proof

Step Hyp Ref Expression
1 hlatjcl.b B = Base K
2 hlatjcl.j ˙ = join K
3 hlatjcl.a A = Atoms K
4 hllat K HL K Lat
5 1 3 atbase X A X B
6 1 3 atbase Y A Y B
7 1 2 latjcl K Lat X B Y B X ˙ Y B
8 4 5 6 7 syl3an K HL X A Y A X ˙ Y B