This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clatglbcl2

Description: Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 13-Sep-2018)

Ref Expression
Hypotheses clatglbcl.b ⊢ B = Base K
clatglbcl.g ⊢ G = glb ⁡ K
Assertion clatglbcl2 ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ G

Proof

Step Hyp Ref Expression
1 clatglbcl.b ⊢ B = Base K
2 clatglbcl.g ⊢ G = glb ⁡ K
3 1 fvexi ⊢ B ∈ V
4 3 elpw2 ⊢ S ∈ 𝒫 B ↔ S ⊆ B
5 4 biimpri ⊢ S ⊆ B → S ∈ 𝒫 B
6 5 adantl ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ 𝒫 B
7 eqid ⊢ lub ⁡ K = lub ⁡ K
8 1 7 2 isclat ⊢ K ∈ CLat ↔ K ∈ Poset ∧ dom ⁡ lub ⁡ K = 𝒫 B ∧ dom ⁡ G = 𝒫 B
9 simprr ⊢ K ∈ Poset ∧ dom ⁡ lub ⁡ K = 𝒫 B ∧ dom ⁡ G = 𝒫 B → dom ⁡ G = 𝒫 B
10 8 9 sylbi ⊢ K ∈ CLat → dom ⁡ G = 𝒫 B
11 10 adantr ⊢ K ∈ CLat ∧ S ⊆ B → dom ⁡ G = 𝒫 B
12 6 11 eleqtrrd ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ G