This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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