# Metamath Proof Explorer

## Theorem latlem12

Description: An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011)

Ref Expression
Hypotheses latmle.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
latmle.l
latmle.m
Assertion latlem12

### Proof

Step Hyp Ref Expression
1 latmle.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 latmle.l
3 latmle.m
4 latpos ${⊢}{K}\in \mathrm{Lat}\to {K}\in \mathrm{Poset}$
5 4 adantr ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{Poset}$
6 simpr2 ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {B}$
7 simpr3 ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$
8 simpr1 ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {B}$
9 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
10 simpl ${⊢}\left({K}\in \mathrm{Lat}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{Lat}$
11 1 9 3 10 6 7 latcl2
12 11 simprd
13 1 2 3 5 6 7 8 12 meetle