Theorem latnlemlt

Description: Negation of "less than or equal to" expressed in terms of meet and less-than. ( nssinpss analog.) (Contributed by NM, 5-Feb-2012)

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

Proof

Step	Hyp	Ref	Expression
1		latnlemlt.b	|- B = ( Base ` K )
2		latnlemlt.l	|- .<_ = ( le ` K )
3		latnlemlt.s	|- .< = ( lt ` K )
4		latnlemlt.m	|- ./\ = ( meet ` K )
5	1 2 4	latmle1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ X )
6	5	biantrurd	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) =/= X <-> ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) =/= X ) ) )
7	1 2 4	latleeqm1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X ./\ Y ) = X ) )
8	7	necon3bbid	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( -. X .<_ Y <-> ( X ./\ Y ) =/= X ) )
9		simp1	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Lat )
10	1 4	latmcl	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
11		simp2	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X e. B )
12	2 3	pltval	|- ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ X e. B ) -> ( ( X ./\ Y ) .< X <-> ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) =/= X ) ) )
13	9 10 11 12	syl3anc	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) .< X <-> ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) =/= X ) ) )
14	6 8 13	3bitr4d	|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( -. X .<_ Y <-> ( X ./\ Y ) .< X ) )