Theorem glble

Description: The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011) (Revised by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	glbprop.b	|- B = ( Base ` K )
	glbprop.l	|- .<_ = ( le ` K )
	glbprop.u	|- U = ( glb ` K )
	glbprop.k	|- ( ph -> K e. V )
	glbprop.s	|- ( ph -> S e. dom U )
	glble.x	|- ( ph -> X e. S )
Assertion	glble	|- ( ph -> ( U ` S ) .<_ X )

Proof

Step	Hyp	Ref	Expression
1		glbprop.b	|- B = ( Base ` K )
2		glbprop.l	|- .<_ = ( le ` K )
3		glbprop.u	|- U = ( glb ` K )
4		glbprop.k	|- ( ph -> K e. V )
5		glbprop.s	|- ( ph -> S e. dom U )
6		glble.x	|- ( ph -> X e. S )
7		breq2	|- ( y = X -> ( ( U ` S ) .<_ y <-> ( U ` S ) .<_ X ) )
8	1 2 3 4 5	glbprop	|- ( ph -> ( A. y e. S ( U ` S ) .<_ y /\ A. z e. B ( A. y e. S z .<_ y -> z .<_ ( U ` S ) ) ) )
9	8	simpld	|- ( ph -> A. y e. S ( U ` S ) .<_ y )
10	7 9 6	rspcdva	|- ( ph -> ( U ` S ) .<_ X )