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={\mathrm{Base}}_K$$
	latnlemlt.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	latnlemlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	latnlemlt.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
Assertion	latnlemlt	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\neg X\underset{\dot{}}{\le }Y\leftrightarrow \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{<}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		latnlemlt.b	$$⊢B={\mathrm{Base}}_K$$
2		latnlemlt.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		latnlemlt.s	$$⊢\underset{\dot{}}{<}={<}_K$$
4		latnlemlt.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5	1 2 4	latmle1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X$$
6	5	biantrurd	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\wedge }Y\ne X\leftrightarrow \left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\wedge }Y\ne X\right)\right)$$
7	1 2 4	latleeqm1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow X\underset{\dot{}}{\wedge }Y=X\right)$$
8	7	necon3bbid	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\neg X\underset{\dot{}}{\le }Y\leftrightarrow X\underset{\dot{}}{\wedge }Y\ne X\right)$$
9		simp1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to K\in \mathrm{Lat}$$
10	1 4	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\wedge }Y\in B$$
11		simp2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
12	2 3	pltval	$$⊢\left(K\in \mathrm{Lat}\wedge X\underset{\dot{}}{\wedge }Y\in B\wedge X\in B\right)\to \left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{<}X\leftrightarrow \left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\wedge }Y\ne X\right)\right)$$
13	9 10 11 12	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{<}X\leftrightarrow \left(\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\le }X\wedge X\underset{\dot{}}{\wedge }Y\ne X\right)\right)$$
14	6 8 13	3bitr4d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\neg X\underset{\dot{}}{\le }Y\leftrightarrow \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{<}X\right)$$