Theorem lubl

Description: The LUB of a complete lattice subset is the least 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	lubl	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\wedge X\in B\right)\to \left(\forall y\in Sy\underset{\dot{}}{\le }X\to U\left(S\right)\underset{\dot{}}{\le }X\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	simprd	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\right)\to \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to U\left(S\right)\underset{\dot{}}{\le }z\right)$$
6		breq2	$$⊢z=X\to \left(y\underset{\dot{}}{\le }z\leftrightarrow y\underset{\dot{}}{\le }X\right)$$
7	6	ralbidv	$$⊢z=X\to \left(\forall y\in Sy\underset{\dot{}}{\le }z\leftrightarrow \forall y\in Sy\underset{\dot{}}{\le }X\right)$$
8		breq2	$$⊢z=X\to \left(U\left(S\right)\underset{\dot{}}{\le }z\leftrightarrow U\left(S\right)\underset{\dot{}}{\le }X\right)$$
9	7 8	imbi12d	$$⊢z=X\to \left(\left(\forall y\in Sy\underset{\dot{}}{\le }z\to U\left(S\right)\underset{\dot{}}{\le }z\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }X\to U\left(S\right)\underset{\dot{}}{\le }X\right)\right)$$
10	9	rspccva	$$⊢\left(\forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to U\left(S\right)\underset{\dot{}}{\le }z\right)\wedge X\in B\right)\to \left(\forall y\in Sy\underset{\dot{}}{\le }X\to U\left(S\right)\underset{\dot{}}{\le }X\right)$$
11	5 10	stoic3	$$⊢\left(K\in \mathrm{CLat}\wedge S\subseteq B\wedge X\in B\right)\to \left(\forall y\in Sy\underset{\dot{}}{\le }X\to U\left(S\right)\underset{\dot{}}{\le }X\right)$$