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