Metamath Proof Explorer


Theorem latlej2

Description: A join's second argument is less than or equal to the join. ( chub2 analog.) (Contributed by NM, 17-Sep-2011)

Ref Expression
Hypotheses latlej.b B=BaseK
latlej.l ˙=K
latlej.j ˙=joinK
Assertion latlej2 KLatXBYBY˙X˙Y

Proof

Step Hyp Ref Expression
1 latlej.b B=BaseK
2 latlej.l ˙=K
3 latlej.j ˙=joinK
4 simp1 KLatXBYBKLat
5 simp2 KLatXBYBXB
6 simp3 KLatXBYBYB
7 eqid meetK=meetK
8 1 3 7 4 5 6 latcl2 KLatXBYBXYdom˙XYdommeetK
9 8 simpld KLatXBYBXYdom˙
10 1 2 3 4 5 6 9 lejoin2 KLatXBYBY˙X˙Y