Theorem latleeqj2

Description: "Less than or equal to" in terms of join. ( chlejb2 analog.) (Contributed by NM, 14-Nov-2011)

	Ref	Expression
Hypotheses	latlej.b	|- B = ( Base ` K )
	latlej.l	|- .<_ = ( le ` K )
	latlej.j	|- .\/ = ( join ` K )
Assertion	latleeqj2	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( Y .\/ X ) = Y ) )

Proof

Step	Hyp	Ref	Expression
1		latlej.b	|- B = ( Base ` K )
2		latlej.l	|- .<_ = ( le ` K )
3		latlej.j	|- .\/ = ( join ` K )
4	1 2 3	latleeqj1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X .\/ Y ) = Y ) )
5	1 3	latjcom	|- ( ( 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 ) = Y <-> ( Y .\/ X ) = Y ) )
7	4 6	bitrd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( Y .\/ X ) = Y ) )