Theorem glbeu

Description: Unique existence proper of a member of the domain of the greatest lower bound function of a poset. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	glbval.b	$$⊢B={\mathrm{Base}}_K$$
	glbval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	glbval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	glbval.p	$$⊢\psi \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)$$
	glbva.k	$$⊢\phi \to K\in V$$
	glbval.s	$$⊢\phi \to S\in \mathrm{dom}G$$
Assertion	glbeu	$$⊢\phi \to \exists !x\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		glbval.b	$$⊢B={\mathrm{Base}}_K$$
2		glbval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		glbval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
4		glbval.p	$$⊢\psi \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)$$
5		glbva.k	$$⊢\phi \to K\in V$$
6		glbval.s	$$⊢\phi \to S\in \mathrm{dom}G$$
7	1 2 3 4 5	glbeldm	$$⊢\phi \to \left(S\in \mathrm{dom}G\leftrightarrow \left(S\subseteq B\wedge \exists !x\in B\psi \right)\right)$$
8	6 7	mpbid	$$⊢\phi \to \left(S\subseteq B\wedge \exists !x\in B\psi \right)$$
9	8	simprd	$$⊢\phi \to \exists !x\in B\psi$$