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 bilanri ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ 𝒫 B
8 1 2 3 isclat ⊢ K ∈ CLat ↔ K ∈ Poset ∧ dom ⁡ U = 𝒫 B ∧ dom ⁡ G = 𝒫 B
9 8 birani ⊢ K ∈ CLat ∧ S ⊆ B → K ∈ Poset ∧ dom ⁡ U = 𝒫 B ∧ dom ⁡ G = 𝒫 B
10 9 simprld ⊢ K ∈ CLat ∧ S ⊆ B → dom ⁡ U = 𝒫 B
11 7 10 eleqtrrd ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ U
12 1 2 4 11 lubcl ⊢ K ∈ CLat ∧ S ⊆ B → U ⁡ S ∈ B
13 9 simprrd ⊢ K ∈ CLat ∧ S ⊆ B → dom ⁡ G = 𝒫 B
14 7 13 eleqtrrd ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ G
15 1 3 4 14 glbcl ⊢ K ∈ CLat ∧ S ⊆ B → G ⁡ S ∈ B
16 12 15 jca ⊢ K ∈ CLat ∧ S ⊆ B → U ⁡ S ∈ B ∧ G ⁡ S ∈ B