Theorem lubeu

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

	Ref	Expression
Hypotheses	lubval.b	$$⊢B={\mathrm{Base}}_K$$
	lubval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	lubval.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	lubval.p	$$⊢\psi \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)$$
	lubval.k	$$⊢\phi \to K\in V$$
	lubeleu.s	$$⊢\phi \to S\in \mathrm{dom}U$$
Assertion	lubeu	$$⊢\phi \to \exists !x\in B\psi$$

Proof

Step	Hyp	Ref	Expression
1		lubval.b	$$⊢B={\mathrm{Base}}_K$$
2		lubval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		lubval.u	$$⊢U=\mathrm{lub}\left(K\right)$$
4		lubval.p	$$⊢\psi \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)$$
5		lubval.k	$$⊢\phi \to K\in V$$
6		lubeleu.s	$$⊢\phi \to S\in \mathrm{dom}U$$
7	1 2 3 4 5	lubeldm	$$⊢\phi \to \left(S\in \mathrm{dom}U\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$$