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 = Base K
latlej.l ˙ = K
latlej.j ˙ = join K
Assertion latlej2 K Lat X B Y B Y ˙ X ˙ Y

Proof

Step Hyp Ref Expression
1 latlej.b B = Base K
2 latlej.l ˙ = K
3 latlej.j ˙ = join K
4 simp1 K Lat X B Y B K Lat
5 simp2 K Lat X B Y B X B
6 simp3 K Lat X B Y B Y B
7 eqid meet K = meet K
8 1 3 7 4 5 6 latcl2 K Lat X B Y B X Y dom ˙ X Y dom meet K
9 8 simpld K Lat X B Y B X Y dom ˙
10 1 2 3 4 5 6 9 lejoin2 K Lat X B Y B Y ˙ X ˙ Y