Theorem latleeqj1

Description: "Less than or equal to" in terms of join. ( chlejb1 analog.) (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	latlej.b	$$⊢B={\mathrm{Base}}_K$$
	latlej.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	latlej.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
Assertion	latleeqj1	$$⊢\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{}}{\vee }Y=Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		latlej.b	$$⊢B={\mathrm{Base}}_K$$
2		latlej.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		latlej.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4	1 2	latref	$$⊢\left(K\in \mathrm{Lat}\wedge Y\in B\right)\to Y\underset{\dot{}}{\le }Y$$
5	4	3adant2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to Y\underset{\dot{}}{\le }Y$$
6	5	biantrud	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }Y\right)\right)$$
7		simp1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to K\in \mathrm{Lat}$$
8		simp2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
9		simp3	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to Y\in B$$
10	1 2 3	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(X\in B\wedge Y\in B\wedge Y\in B\right)\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }Y\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\right)$$
11	7 8 9 9 10	syl13anc	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }Y\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\right)$$
12	6 11	bitrd	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\right)$$
13	1 2 3	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)$$
14	13	biantrud	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\leftrightarrow \left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\right)$$
15	12 14	bitrd	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow \left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\right)$$
16		latpos	$$⊢K\in \mathrm{Lat}\to K\in \mathrm{Poset}$$
17	16	3ad2ant1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to K\in \mathrm{Poset}$$
18	1 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{\vee }Y\in B$$
19	1 2	posasymb	$$⊢\left(K\in \mathrm{Poset}\wedge X\underset{\dot{}}{\vee }Y\in B\wedge Y\in B\right)\to \left(\left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }Y=Y\right)$$
20	17 18 9 19	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(\left(\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Y\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }Y=Y\right)$$
21	15 20	bitrd	$$⊢\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{}}{\vee }Y=Y\right)$$