# Metamath Proof Explorer

## Theorem clatlem

Description: Lemma for properties of a complete lattice. (Contributed by NM, 14-Sep-2011)

Ref Expression
Hypotheses clatlem.b $⊢ B = Base K$
clatlem.u $⊢ U = lub ⁡ K$
clatlem.g $⊢ G = glb ⁡ K$
Assertion clatlem $⊢ K ∈ CLat ∧ S ⊆ B → U ⁡ S ∈ B ∧ G ⁡ S ∈ B$

### Proof

Step Hyp Ref Expression
1 clatlem.b $⊢ B = Base K$
2 clatlem.u $⊢ U = lub ⁡ K$
3 clatlem.g $⊢ G = glb ⁡ K$
4 simpl $⊢ K ∈ CLat ∧ S ⊆ B → K ∈ CLat$
5 1 fvexi $⊢ B ∈ V$
6 5 elpw2 $⊢ S ∈ 𝒫 B ↔ S ⊆ B$
7 6 biimpri $⊢ S ⊆ B → S ∈ 𝒫 B$
8 7 adantl $⊢ K ∈ CLat ∧ S ⊆ B → S ∈ 𝒫 B$
9 1 2 3 isclat $⊢ K ∈ CLat ↔ K ∈ Poset ∧ dom ⁡ U = 𝒫 B ∧ dom ⁡ G = 𝒫 B$
10 9 biimpi $⊢ K ∈ CLat → K ∈ Poset ∧ dom ⁡ U = 𝒫 B ∧ dom ⁡ G = 𝒫 B$
11 10 adantr $⊢ K ∈ CLat ∧ S ⊆ B → K ∈ Poset ∧ dom ⁡ U = 𝒫 B ∧ dom ⁡ G = 𝒫 B$
12 11 simprld $⊢ K ∈ CLat ∧ S ⊆ B → dom ⁡ U = 𝒫 B$
13 8 12 eleqtrrd $⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ U$
14 1 2 4 13 lubcl $⊢ K ∈ CLat ∧ S ⊆ B → U ⁡ S ∈ B$
15 11 simprrd $⊢ K ∈ CLat ∧ S ⊆ B → dom ⁡ G = 𝒫 B$
16 8 15 eleqtrrd $⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ G$
17 1 3 4 16 glbcl $⊢ K ∈ CLat ∧ S ⊆ B → G ⁡ S ∈ B$
18 14 17 jca $⊢ K ∈ CLat ∧ S ⊆ B → U ⁡ S ∈ B ∧ G ⁡ S ∈ B$