Theorem latleeqm1

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	latleeqm1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X ./\ Y ) = 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	latref	|- ( ( K e. Lat /\ X e. B ) -> X .<_ X )
5	4	3adant3	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X .<_ X )
6	5	biantrurd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X .<_ X /\ X .<_ Y ) ) )
7		simp1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Lat )
8		simp2	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X e. B )
9		simp3	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y e. B )
10	1 2 3	latlem12	|- ( ( K e. Lat /\ ( X e. B /\ X e. B /\ Y e. B ) ) -> ( ( X .<_ X /\ X .<_ Y ) <-> X .<_ ( X ./\ Y ) ) )
11	7 8 8 9 10	syl13anc	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X .<_ X /\ X .<_ Y ) <-> X .<_ ( X ./\ Y ) ) )
12	6 11	bitrd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> X .<_ ( X ./\ Y ) ) )
13	1 2 3	latmle1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ X )
14	13	biantrurd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ ( X ./\ Y ) <-> ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) ) )
15	12 14	bitrd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) ) )
16		latpos	|- ( K e. Lat -> K e. Poset )
17	16	3ad2ant1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Poset )
18	1 3	latmcl	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
19	1 2	posasymb	|- ( ( K e. Poset /\ ( X ./\ Y ) e. B /\ X e. B ) -> ( ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) <-> ( X ./\ Y ) = X ) )
20	17 18 8 19	syl3anc	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) <-> ( X ./\ Y ) = X ) )
21	15 20	bitrd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X ./\ Y ) = X ) )