Theorem luble

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

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

Proof

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