Theorem latlej1

Description: A join's first argument is less than or equal to the join. ( chub1 analog.) (Contributed by NM, 17-Sep-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	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)$$

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		simp1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to K\in \mathrm{Lat}$$
5		simp2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to X\in B$$
6		simp3	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to Y\in B$$
7		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
8	1 3 7 4 5 6	latcl2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to \left(⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }\wedge ⟨X,Y⟩\in \mathrm{dom}\mathrm{meet}\left(K\right)\right)$$
9	8	simpld	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Y\in B\right)\to ⟨X,Y⟩\in \mathrm{dom}\underset{\dot{}}{\vee }$$
10	1 2 3 4 5 6 9	lejoin1	$$⊢\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)$$