Theorem lubl

Description: The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011)

	Ref	Expression
Hypotheses	lublem.b	|- B = ( Base ` K )
	lublem.l	|- .<_ = ( le ` K )
	lublem.u	|- U = ( lub ` K )
Assertion	lubl	|- ( ( K e. CLat /\ S C_ B /\ X e. B ) -> ( A. y e. S y .<_ X -> ( U ` S ) .<_ X ) )

Proof

Step	Hyp	Ref	Expression
1		lublem.b	|- B = ( Base ` K )
2		lublem.l	|- .<_ = ( le ` K )
3		lublem.u	|- U = ( lub ` K )
4	1 2 3	lublem	|- ( ( K e. CLat /\ S C_ B ) -> ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) )
5	4	simprd	|- ( ( K e. CLat /\ S C_ B ) -> A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) )
6		breq2	|- ( z = X -> ( y .<_ z <-> y .<_ X ) )
7	6	ralbidv	|- ( z = X -> ( A. y e. S y .<_ z <-> A. y e. S y .<_ X ) )
8		breq2	|- ( z = X -> ( ( U ` S ) .<_ z <-> ( U ` S ) .<_ X ) )
9	7 8	imbi12d	|- ( z = X -> ( ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) <-> ( A. y e. S y .<_ X -> ( U ` S ) .<_ X ) ) )
10	9	rspccva	|- ( ( A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) /\ X e. B ) -> ( A. y e. S y .<_ X -> ( U ` S ) .<_ X ) )
11	5 10	stoic3	|- ( ( K e. CLat /\ S C_ B /\ X e. B ) -> ( A. y e. S y .<_ X -> ( U ` S ) .<_ X ) )