Step |
Hyp |
Ref |
Expression |
1 |
|
glbs.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
glbs.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
glbs.g |
⊢ 𝐺 = ( glb ‘ 𝐾 ) |
4 |
|
glbs.k |
⊢ ( 𝜑 → 𝐾 ∈ 𝑉 ) |
5 |
|
glbs.s |
⊢ ( 𝜑 → 𝑆 ∈ dom 𝐺 ) |
6 |
|
biid |
⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) |
7 |
1 2 3 6 4
|
glbeldm |
⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) ) |
8 |
5 7
|
mpbid |
⊢ ( 𝜑 → ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) ) ) |
9 |
8
|
simpld |
⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 ) |