Theorem glbelss

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

	Ref	Expression
Hypotheses	glbs.b	|- B = ( Base ` K )
	glbs.l	|- .<_ = ( le ` K )
	glbs.g	|- G = ( glb ` K )
	glbs.k	|- ( ph -> K e. V )
	glbs.s	|- ( ph -> S e. dom G )
Assertion	glbelss	|- ( ph -> S C_ B )

Proof

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