Metamath Proof Explorer


Theorem latleeqm1

Description: "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011)

Ref Expression
Hypotheses latmle.b B=BaseK
latmle.l ˙=K
latmle.m ˙=meetK
Assertion latleeqm1 KLatXBYBX˙YX˙Y=X

Proof

Step Hyp Ref Expression
1 latmle.b B=BaseK
2 latmle.l ˙=K
3 latmle.m ˙=meetK
4 1 2 latref KLatXBX˙X
5 4 3adant3 KLatXBYBX˙X
6 5 biantrurd KLatXBYBX˙YX˙XX˙Y
7 simp1 KLatXBYBKLat
8 simp2 KLatXBYBXB
9 simp3 KLatXBYBYB
10 1 2 3 latlem12 KLatXBXBYBX˙XX˙YX˙X˙Y
11 7 8 8 9 10 syl13anc KLatXBYBX˙XX˙YX˙X˙Y
12 6 11 bitrd KLatXBYBX˙YX˙X˙Y
13 1 2 3 latmle1 KLatXBYBX˙Y˙X
14 13 biantrurd KLatXBYBX˙X˙YX˙Y˙XX˙X˙Y
15 12 14 bitrd KLatXBYBX˙YX˙Y˙XX˙X˙Y
16 latpos KLatKPoset
17 16 3ad2ant1 KLatXBYBKPoset
18 1 3 latmcl KLatXBYBX˙YB
19 1 2 posasymb KPosetX˙YBXBX˙Y˙XX˙X˙YX˙Y=X
20 17 18 8 19 syl3anc KLatXBYBX˙Y˙XX˙X˙YX˙Y=X
21 15 20 bitrd KLatXBYBX˙YX˙Y=X