Metamath Proof Explorer


Theorem latmidm

Description: Lattice meet is idempotent. Analogue of inidm . (Contributed by NM, 8-Nov-2011)

Ref Expression
Hypotheses latmidm.b B=BaseK
latmidm.m ˙=meetK
Assertion latmidm KLatXBX˙X=X

Proof

Step Hyp Ref Expression
1 latmidm.b B=BaseK
2 latmidm.m ˙=meetK
3 eqid K=K
4 simpl KLatXBKLat
5 1 2 latmcl KLatXBXBX˙XB
6 5 3anidm23 KLatXBX˙XB
7 simpr KLatXBXB
8 1 3 2 latmle1 KLatXBXBX˙XKX
9 8 3anidm23 KLatXBX˙XKX
10 1 3 latref KLatXBXKX
11 1 3 2 latlem12 KLatXBXBXBXKXXKXXKX˙X
12 4 7 7 7 11 syl13anc KLatXBXKXXKXXKX˙X
13 10 10 12 mpbi2and KLatXBXKX˙X
14 1 3 4 6 7 9 13 latasymd KLatXBX˙X=X