Theorem lublem

Description: Lemma for the least upper bound properties in a complete lattice. (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	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)$$

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		simpl	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to K\in \mathrm{CLat}$$
5	1 3	clatlubcl2	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to S\in \mathrm{dom}U$$
6	1 2 3 4 5	lubprop	$$⊢\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)$$