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