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 = ( Base ` K )
	lubval.l	|- .<_ = ( le ` K )
	lubval.u	|- U = ( lub ` K )
	lubval.p	|- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
	lubval.k	|- ( ph -> K e. V )
	lubeleu.s	|- ( ph -> S e. dom U )
Assertion	lubeu	|- ( ph -> E! x e. B ps )

Proof

Step	Hyp	Ref	Expression
1		lubval.b	|- B = ( Base ` K )
2		lubval.l	|- .<_ = ( le ` K )
3		lubval.u	|- U = ( lub ` K )
4		lubval.p	|- ( ps <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
5		lubval.k	|- ( ph -> K e. V )
6		lubeleu.s	|- ( ph -> S e. dom U )
7	1 2 3 4 5	lubeldm	|- ( ph -> ( S e. dom U <-> ( 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 )