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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lublem.l	⊢ ≤ = ( le ‘ 𝐾 )
	lublem.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion	lubel	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → 𝑋 ≤ ( 𝑈 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		lublem.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lublem.l	⊢ ≤ = ( le ‘ 𝐾 )
3		lublem.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
4		clatl	⊢ ( 𝐾 ∈ CLat → 𝐾 ∈ Lat )
5		ssel	⊢ ( 𝑆 ⊆ 𝐵 → ( 𝑋 ∈ 𝑆 → 𝑋 ∈ 𝐵 ) )
6	5	impcom	⊢ ( ( 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → 𝑋 ∈ 𝐵 )
7	1 3	lubsn	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑋 } ) = 𝑋 )
8	4 6 7	syl2an	⊢ ( ( 𝐾 ∈ CLat ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) ) → ( 𝑈 ‘ { 𝑋 } ) = 𝑋 )
9	8	3impb	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑈 ‘ { 𝑋 } ) = 𝑋 )
10		snssi	⊢ ( 𝑋 ∈ 𝑆 → { 𝑋 } ⊆ 𝑆 )
11	1 2 3	lubss	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ { 𝑋 } ⊆ 𝑆 ) → ( 𝑈 ‘ { 𝑋 } ) ≤ ( 𝑈 ‘ 𝑆 ) )
12	10 11	syl3an3	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑈 ‘ { 𝑋 } ) ≤ ( 𝑈 ‘ 𝑆 ) )
13	12	3com23	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑈 ‘ { 𝑋 } ) ≤ ( 𝑈 ‘ 𝑆 ) )
14	9 13	eqbrtrrd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → 𝑋 ≤ ( 𝑈 ‘ 𝑆 ) )