Theorem lublem

Description: Lemma for the least upper bound properties in a complete lattice. (Contributed by NM, 19-Oct-2011)

	Ref	Expression
Hypotheses	lublem.b	|- B = ( Base ` K )
	lublem.l	|- .<_ = ( le ` K )
	lublem.u	|- U = ( lub ` K )
Assertion	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 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lublem.b	|- B = ( Base ` K )
2		lublem.l	|- .<_ = ( le ` K )
3		lublem.u	|- U = ( lub ` K )
4		simpl	|- ( ( K e. CLat /\ S C_ B ) -> K e. CLat )
5	1 3	clatlubcl2	|- ( ( K e. CLat /\ S C_ B ) -> S e. dom U )
6	1 2 3 4 5	lubprop	|- ( ( 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 ) ) )