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 = ( Base ` K )
	glbval.l	|- .<_ = ( le ` K )
	glbval.g	|- G = ( glb ` K )
	glbval.p	|- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
	glbva.k	|- ( ph -> K e. V )
	glbval.s	|- ( ph -> S e. dom G )
Assertion	glbeu	|- ( ph -> E! x e. B ps )

Proof

Step	Hyp	Ref	Expression
1		glbval.b	|- B = ( Base ` K )
2		glbval.l	|- .<_ = ( le ` K )
3		glbval.g	|- G = ( glb ` K )
4		glbval.p	|- ( ps <-> ( A. y e. S x .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ x ) ) )
5		glbva.k	|- ( ph -> K e. V )
6		glbval.s	|- ( ph -> S e. dom G )
7	1 2 3 4 5	glbeldm	|- ( ph -> ( S e. dom G <-> ( S C_ B /\ E! x e. B ps ) ) )
8	6 7	mpbid	|- ( ph -> ( S C_ B /\ E! x e. B ps ) )
9	8	simprd	|- ( ph -> E! x e. B ps )