Theorem latnle

Description: Equivalent expressions for "not less than" in a lattice. ( chnle analog.) (Contributed by NM, 16-Nov-2011)

	Ref	Expression
Hypotheses	latnle.b	$$⊢B={\mathrm{Base}}_K$$
	latnle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	latnle.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	latnle.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
Assertion	latnle	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\neg Y\underset{\dot{}}{\le }X\leftrightarrow X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		latnle.b	$$⊢B={\mathrm{Base}}_K$$
2		latnle.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		latnle.s	$$⊢\underset{\dot{}}{<}={<}_K$$
4		latnle.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
5	1 2 4	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)$$
6	5	biantrurd	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\ne X\underset{\dot{}}{\vee }Y\leftrightarrow \left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge X\ne X\underset{\dot{}}{\vee }Y\right)\right)$$
7	1 2 4	latleeqj1	$$⊢\left(K\in \mathrm{Lat}\wedge Y\in B\wedge X\in B\right)\to \left(Y\underset{\dot{}}{\le }X\leftrightarrow Y\underset{\dot{}}{\vee }X=X\right)$$
8	7	3com23	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(Y\underset{\dot{}}{\le }X\leftrightarrow Y\underset{\dot{}}{\vee }X=X\right)$$
9		eqcom	$$⊢Y\underset{\dot{}}{\vee }X=X\leftrightarrow X=Y\underset{\dot{}}{\vee }X$$
10	8 9	bitrdi	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(Y\underset{\dot{}}{\le }X\leftrightarrow X=Y\underset{\dot{}}{\vee }X\right)$$
11	1 4	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\vee }Y=Y\underset{\dot{}}{\vee }X$$
12	11	eqeq2d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X=X\underset{\dot{}}{\vee }Y\leftrightarrow X=Y\underset{\dot{}}{\vee }X\right)$$
13	10 12	bitr4d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(Y\underset{\dot{}}{\le }X\leftrightarrow X=X\underset{\dot{}}{\vee }Y\right)$$
14	13	necon3bbid	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\neg Y\underset{\dot{}}{\le }X\leftrightarrow X\ne X\underset{\dot{}}{\vee }Y\right)$$
15	1 4	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\vee }Y\in B$$
16	2 3	pltval	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge X\underset{\dot{}}{\vee }Y\in B\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }Y\right)\leftrightarrow \left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge X\ne X\underset{\dot{}}{\vee }Y\right)\right)$$
17	15 16	syld3an3	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }Y\right)\leftrightarrow \left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\wedge X\ne X\underset{\dot{}}{\vee }Y\right)\right)$$
18	6 14 17	3bitr4d	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\neg Y\underset{\dot{}}{\le }X\leftrightarrow X\underset{\dot{}}{<}\left(X\underset{\dot{}}{\vee }Y\right)\right)$$