# 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
`|- .<_ = ( le ` K )`
latmle.m
`|- ./\ = ( meet ` K )`
Assertion latmle2
`|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ Y )`

### Proof

Step Hyp Ref Expression
1 latmle.b
` |-  B = ( Base ` K )`
2 latmle.l
` |-  .<_ = ( le ` K )`
3 latmle.m
` |-  ./\ = ( meet ` K )`
4 simp1
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Lat )`
5 simp2
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X e. B )`
6 simp3
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y e. B )`
7 eqid
` |-  ( join ` K ) = ( join ` K )`
8 1 7 3 4 5 6 latcl2
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( <. X , Y >. e. dom ( join ` K ) /\ <. X , Y >. e. dom ./\ ) )`
9 8 simprd
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> <. X , Y >. e. dom ./\ )`
10 1 2 3 4 5 6 9 lemeet2
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ Y )`