Theorem lubelss

Description: A member of the domain of the least upper bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		lubs.b	$$⊢B={\mathrm{Base}}_K$$
2		lubs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lubs.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lubs.k	$$⊢\phi \to K\in V$$
5		lubs.s	$$⊢\phi \to S\in \mathrm{dom}U$$
6		biid	$$⊢\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\leftrightarrow \left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)$$
7	1 2 3 6 4	lubeldm	$$⊢\phi \to \left(S\in \mathrm{dom}U\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)\right)$$
8	5 7	mpbid	$$⊢\phi \to \left(S\subseteq B\wedge \exists !x\in B\left(\forall y\in Sy\underset{\dot{}}{\le }x\wedge \forall z\in B\left(\forall y\in Sy\underset{\dot{}}{\le }z\to x\underset{\dot{}}{\le }z\right)\right)\right)$$
9	8	simpld	$$⊢\phi \to S\subseteq B$$