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

Metamath Proof Explorer

Theorem lubel

Description: An element of a set is less than or equal to the least upper bound of the set. (Contributed by NM, 21-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 lublem.b 
 |-  B = ( Base ` K )
2 lublem.l 
 |-  .<_ = ( le ` K )
3 lublem.u 
 |-  U = ( lub ` K )
4 clatl 
 |-  ( K e. CLat -> K e. Lat )
5 ssel 
 |-  ( S C_ B -> ( X e. S -> X e. B ) )
6 5 impcom 
 |-  ( ( X e. S /\ S C_ B ) -> X e. B )
7 1 3 lubsn 
 |-  ( ( K e. Lat /\ X e. B ) -> ( U ` { X } ) = X )
8 4 6 7 syl2an 
 |-  ( ( K e. CLat /\ ( X e. S /\ S C_ B ) ) -> ( U ` { X } ) = X )
9 8 3impb 
 |-  ( ( K e. CLat /\ X e. S /\ S C_ B ) -> ( U ` { X } ) = X )
10 snssi 
 |-  ( X e. S -> { X } C_ S )
11 1 2 3 lubss 
 |-  ( ( K e. CLat /\ S C_ B /\ { X } C_ S ) -> ( U ` { X } ) .<_ ( U ` S ) )
12 10 11 syl3an3 
 |-  ( ( K e. CLat /\ S C_ B /\ X e. S ) -> ( U ` { X } ) .<_ ( U ` S ) )
13 12 3com23 
 |-  ( ( K e. CLat /\ X e. S /\ S C_ B ) -> ( U ` { X } ) .<_ ( U ` S ) )
14 9 13 eqbrtrrd 
 |-  ( ( K e. CLat /\ X e. S /\ S C_ B ) -> X .<_ ( U ` S ) )