Theorem lubel

Description: An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	lublem.b	$$⊢B={\mathrm{Base}}_K$$
	lublem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lublem.u	$$⊢U=\mathrm{lub}\left(K\right)$$
Assertion	lubel	$$⊢\left(K\in \mathrm{CLat}\wedge X\in S\wedge S\subseteq B\right)\to X\underset{\dot{}}{\le }U\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		lublem.b	$$⊢B={\mathrm{Base}}_K$$
2		lublem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lublem.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		clatl	$$⊢K\in \mathrm{CLat}\to K\in \mathrm{Lat}$$
5		ssel	$$⊢S\subseteq B\to \left(X\in S\to X\in B\right)$$
6	5	impcom	$$⊢\left(X\in S\wedge S\subseteq B\right)\to X\in B$$
7	1 3	lubsn	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to U\left(\left\{X\right\}\right)=X$$
8	4 6 7	syl2an	$$⊢\left(K\in \mathrm{CLat}\wedge \left(X\in S\wedge S\subseteq B\right)\right)\to U\left(\left\{X\right\}\right)=X$$
9	8	3impb	$$⊢\left(K\in \mathrm{CLat}\wedge X\in S\wedge S\subseteq B\right)\to U\left(\left\{X\right\}\right)=X$$
10		snssi	$$⊢X\in S\to \left\{X\right\}\subseteq S$$
11	1 2 3	lubss	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\wedge \left\{X\right\}\subseteq S\right)\to U\left(\left\{X\right\}\right)\underset{\dot{}}{\le }U\left(S\right)$$
12	10 11	syl3an3	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\wedge X\in S\right)\to U\left(\left\{X\right\}\right)\underset{\dot{}}{\le }U\left(S\right)$$
13	12	3com23	$$⊢\left(K\in \mathrm{CLat}\wedge X\in S\wedge S\subseteq B\right)\to U\left(\left\{X\right\}\right)\underset{\dot{}}{\le }U\left(S\right)$$
14	9 13	eqbrtrrd	$$⊢\left(K\in \mathrm{CLat}\wedge X\in S\wedge S\subseteq B\right)\to X\underset{\dot{}}{\le }U\left(S\right)$$