Theorem latleeqm2

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

	Ref	Expression
Hypotheses	latmle.b	|- B = ( Base ` K )
	latmle.l	|- .<_ = ( le ` K )
	latmle.m	|- ./\ = ( meet ` K )
Assertion	latleeqm2	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( Y ./\ X ) = X ) )

Proof

Step	Hyp	Ref	Expression
1		latmle.b	|- B = ( Base ` K )
2		latmle.l	|- .<_ = ( le ` K )
3		latmle.m	|- ./\ = ( meet ` K )
4	1 2 3	latleeqm1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X ./\ Y ) = X ) )
5	1 3	latmcom	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) = ( Y ./\ X ) )
6	5	eqeq1d	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) = X <-> ( Y ./\ X ) = X ) )
7	4 6	bitrd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( Y ./\ X ) = X ) )