Theorem lubsn

Description: The least upper bound of a singleton. ( chsupsn analog.) (Contributed by NM, 20-Oct-2011)

	Ref	Expression
Hypotheses	lubsn.b	$$⊢B={\mathrm{Base}}_K$$
	lubsn.u	$$⊢U=\mathrm{lub}\left(K\right)$$
Assertion	lubsn	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to U\left(\left\{X\right\}\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		lubsn.b	$$⊢B={\mathrm{Base}}_K$$
2		lubsn.u	$$⊢U=\mathrm{lub}\left(K\right)$$
3		dfsn2	$$⊢\left\{X\right\}=\left\{X,X\right\}$$
4	3	fveq2i	$$⊢U\left(\left\{X\right\}\right)=U\left(\left\{X,X\right\}\right)$$
5		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
6		simpl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to K\in \mathrm{Lat}$$
7		simpr	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to X\in B$$
8	2 5 6 7 7	joinval	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to X\mathrm{join}\left(K\right)X=U\left(\left\{X,X\right\}\right)$$
9	4 8	eqtr4id	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to U\left(\left\{X\right\}\right)=X\mathrm{join}\left(K\right)X$$
10	1 5	latjidm	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to X\mathrm{join}\left(K\right)X=X$$
11	9 10	eqtrd	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\right)\to U\left(\left\{X\right\}\right)=X$$