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