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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
clatlubcl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion clatlubcl2 ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝑈 )

Proof

Step Hyp Ref Expression
1 clatlubcl.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 clatlubcl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
3 1 fvexi ⊢ 𝐵 ∈ V
4 3 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
5 4 biimpri ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 ∈ 𝒫 𝐵 )
6 5 adantl ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ 𝒫 𝐵 )
7 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
8 1 2 7 isclat ⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom ( glb ‘ 𝐾 ) = 𝒫 𝐵 ) ) )
9 simprl ⊢ ( ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom ( glb ‘ 𝐾 ) = 𝒫 𝐵 ) ) → dom 𝑈 = 𝒫 𝐵 )
10 8 9 sylbi ⊢ ( 𝐾 ∈ CLat → dom 𝑈 = 𝒫 𝐵 )
11 10 adantr ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → dom 𝑈 = 𝒫 𝐵 )
12 6 11 eleqtrrd ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝑈 )