Theorem lubelss

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

	Ref	Expression
Hypotheses	lubs.b	|- B = ( Base ` K )
	lubs.l	|- .<_ = ( le ` K )
	lubs.u	|- U = ( lub ` K )
	lubs.k	|- ( ph -> K e. V )
	lubs.s	|- ( ph -> S e. dom U )
Assertion	lubelss	|- ( ph -> S C_ B )

Proof

Step	Hyp	Ref	Expression
1		lubs.b	|- B = ( Base ` K )
2		lubs.l	|- .<_ = ( le ` K )
3		lubs.u	|- U = ( lub ` K )
4		lubs.k	|- ( ph -> K e. V )
5		lubs.s	|- ( ph -> S e. dom U )
6		biid	|- ( ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
7	1 2 3 6 4	lubeldm	|- ( ph -> ( S e. dom U <-> ( S C_ B /\ E! x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) ) )
8	5 7	mpbid	|- ( ph -> ( S C_ B /\ E! x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) )
9	8	simpld	|- ( ph -> S C_ B )