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

Metamath Proof Explorer

Theorem clatlubcl2

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

Ref Expression
Hypotheses clatlubcl.b ⊢ B = Base K
clatlubcl.u ⊢ U = lub ⁡ K
Assertion clatlubcl2 ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ U

Proof

Step Hyp Ref Expression
1 clatlubcl.b ⊢ B = Base K
2 clatlubcl.u ⊢ U = lub ⁡ 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 ⊢ glb ⁡ K = glb ⁡ K
8 1 2 7 isclat ⊢ K ∈ CLat ↔ K ∈ Poset ∧ dom ⁡ U = 𝒫 B ∧ dom ⁡ glb ⁡ K = 𝒫 B
9 simprl ⊢ K ∈ Poset ∧ dom ⁡ U = 𝒫 B ∧ dom ⁡ glb ⁡ K = 𝒫 B → dom ⁡ U = 𝒫 B
10 8 9 sylbi ⊢ K ∈ CLat → dom ⁡ U = 𝒫 B
11 10 adantr ⊢ K ∈ CLat ∧ S ⊆ B → dom ⁡ U = 𝒫 B
12 6 11 eleqtrrd ⊢ K ∈ CLat ∧ S ⊆ B → S ∈ dom ⁡ U