Theorem lubub

Description: The LUB of a complete lattice subset is an upper bound. (Contributed by NM, 19-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	lubub	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\wedge X\in S\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	1 2 3	lublem	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to \left(\forall y\in Sy\underset{\dot{}}{\le }U\left(S\right)\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to U\left(S\right)\underset{\dot{}}{\le }z\right)\right)$$
5	4	simpld	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to \forall y\in Sy\underset{\dot{}}{\le }U\left(S\right)$$
6		breq1	$$⊢y=X\to \left(y\underset{\dot{}}{\le }U\left(S\right)\leftrightarrow X\underset{\dot{}}{\le }U\left(S\right)\right)$$
7	6	rspccva	$$⊢\left(\forall y\in Sy\underset{\dot{}}{\le }U\left(S\right)\wedge X\in S\right)\to X\underset{\dot{}}{\le }U\left(S\right)$$
8	5 7	stoic3	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\wedge X\in S\right)\to X\underset{\dot{}}{\le }U\left(S\right)$$