Metamath Proof Explorer


Theorem latmlej21

Description: Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012)

Ref Expression
Hypotheses latledi.b B=BaseK
latledi.l ˙=K
latledi.j ˙=joinK
latledi.m ˙=meetK
Assertion latmlej21 KLatXBYBZBY˙X˙X˙Z

Proof

Step Hyp Ref Expression
1 latledi.b B=BaseK
2 latledi.l ˙=K
3 latledi.j ˙=joinK
4 latledi.m ˙=meetK
5 1 4 latmcom KLatXBYBX˙Y=Y˙X
6 5 3adant3r3 KLatXBYBZBX˙Y=Y˙X
7 1 2 3 4 latmlej11 KLatXBYBZBX˙Y˙X˙Z
8 6 7 eqbrtrrd KLatXBYBZBY˙X˙X˙Z