Theorem lubcl

Description: The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	lubcl.b	$$⊢B={\mathrm{Base}}_K$$
	lubcl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	lubcl.k	$$⊢\phi \to K\in V$$
	lubcl.s	$$⊢\phi \to S\in \mathrm{dom}U$$
Assertion	lubcl	$$⊢\phi \to U\left(S\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		lubcl.b	$$⊢B={\mathrm{Base}}_K$$
2		lubcl.u	$$⊢U=\mathrm{lub}\left(K\right)$$
3		lubcl.k	$$⊢\phi \to K\in V$$
4		lubcl.s	$$⊢\phi \to S\in \mathrm{dom}U$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6		biid	$$⊢\left(\forall y\in Sy{\le }_{K}x\wedge \forall z\in B\left(\forall y\in Sy{\le }_{K}z\to x{\le }_{K}z\right)\right)\leftrightarrow \left(\forall y\in Sy{\le }_{K}x\wedge \forall z\in B\left(\forall y\in Sy{\le }_{K}z\to x{\le }_{K}z\right)\right)$$
7	1 5 2 3 4	lubelss	$$⊢\phi \to S\subseteq B$$
8	1 5 2 6 3 7	lubval	$$⊢\phi \to U\left(S\right)=\left(\iota x\in B|\left(\forall y\in Sy{\le }_{K}x\wedge \forall z\in B\left(\forall y\in Sy{\le }_{K}z\to x{\le }_{K}z\right)\right)\right)$$
9	1 5 2 6 3 4	lubeu	$$⊢\phi \to \exists !x\in B\left(\forall y\in Sy{\le }_{K}x\wedge \forall z\in B\left(\forall y\in Sy{\le }_{K}z\to x{\le }_{K}z\right)\right)$$
10		riotacl	$$⊢\exists !x\in B\left(\forall y\in Sy{\le }_{K}x\wedge \forall z\in B\left(\forall y\in Sy{\le }_{K}z\to x{\le }_{K}z\right)\right)\to \left(\iota x\in B|\left(\forall y\in Sy{\le }_{K}x\wedge \forall z\in B\left(\forall y\in Sy{\le }_{K}z\to x{\le }_{K}z\right)\right)\right)\in B$$
11	9 10	syl	$$⊢\phi \to \left(\iota x\in B|\left(\forall y\in Sy{\le }_{K}x\wedge \forall z\in B\left(\forall y\in Sy{\le }_{K}z\to x{\le }_{K}z\right)\right)\right)\in B$$
12	8 11	eqeltrd	$$⊢\phi \to U\left(S\right)\in B$$