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 𝐵 = ( 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 ∧ 𝑋𝑆𝑆𝐵 ) → 𝑋 ( 𝑈𝑆 ) )