Metamath Proof Explorer


Theorem latmle2

Description: A meet is less than or equal to its second argument. (Contributed by NM, 21-Oct-2011)

Ref Expression
Hypotheses latmle.b B = Base K
latmle.l ˙ = K
latmle.m ˙ = meet K
Assertion latmle2 K Lat X B Y B X ˙ Y ˙ Y

Proof

Step Hyp Ref Expression
1 latmle.b B = Base K
2 latmle.l ˙ = K
3 latmle.m ˙ = meet 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 join K = join K
8 1 7 3 4 5 6 latcl2 K Lat X B Y B X Y dom join K X Y dom ˙
9 8 simprd K Lat X B Y B X Y dom ˙
10 1 2 3 4 5 6 9 lemeet2 K Lat X B Y B X ˙ Y ˙ Y