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 ⊢ 𝐵 = ( 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 ∧ 𝑋 ∈ 𝑆 ∧ 𝑆 ⊆ 𝐵 ) → 𝑋 ≤ ( 𝑈 ‘ 𝑆 ) )