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