Metamath Proof Explorer


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 ) ) )