Theorem clatlubcl

Description: Any subset of the base set has an LUB in a complete lattice. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	clatlubcl.b	$$⊢B={\mathrm{Base}}_K$$
	clatlubcl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
Assertion	clatlubcl	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to U\left(S\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		clatlubcl.b	$$⊢B={\mathrm{Base}}_K$$
2		clatlubcl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
3		eqid	$$⊢\mathrm{glb}\left(K\right)=\mathrm{glb}\left(K\right)$$
4	1 2 3	clatlem	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to \left(U\left(S\right)\in B\wedge \mathrm{glb}\left(K\right)\left(S\right)\in B\right)$$
5	4	simpld	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to U\left(S\right)\in B$$