Theorem glbelss

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

	Ref	Expression
Hypotheses	glbs.b	$$⊢B={\mathrm{Base}}_K$$
	glbs.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	glbs.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	glbs.k	$$⊢\phi \to K\in V$$
	glbs.s	$$⊢\phi \to S\in \mathrm{dom}G$$
Assertion	glbelss	$$⊢\phi \to S\subseteq B$$

Proof

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