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

Metamath Proof Explorer

Theorem isclat

Description: The predicate "is a complete lattice". (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)

Ref Expression
Hypotheses isclat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
isclat.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
isclat.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
Assertion isclat ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 isclat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isclat.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
3 isclat.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 fveq2 ⊢ ( 𝑙 = 𝐾 → ( lub ‘ 𝑙 ) = ( lub ‘ 𝐾 ) )
5 4 2 eqtr4di ⊢ ( 𝑙 = 𝐾 → ( lub ‘ 𝑙 ) = 𝑈 )
6 5 dmeqd ⊢ ( 𝑙 = 𝐾 → dom ( lub ‘ 𝑙 ) = dom 𝑈 )
7 fveq2 ⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = ( Base ‘ 𝐾 ) )
8 7 1 eqtr4di ⊢ ( 𝑙 = 𝐾 → ( Base ‘ 𝑙 ) = 𝐵 )
9 8 pweqd ⊢ ( 𝑙 = 𝐾 → 𝒫 ( Base ‘ 𝑙 ) = 𝒫 𝐵 )
10 6 9 eqeq12d ⊢ ( 𝑙 = 𝐾 → ( dom ( lub ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ↔ dom 𝑈 = 𝒫 𝐵 ) )
11 fveq2 ⊢ ( 𝑙 = 𝐾 → ( glb ‘ 𝑙 ) = ( glb ‘ 𝐾 ) )
12 11 3 eqtr4di ⊢ ( 𝑙 = 𝐾 → ( glb ‘ 𝑙 ) = 𝐺 )
13 12 dmeqd ⊢ ( 𝑙 = 𝐾 → dom ( glb ‘ 𝑙 ) = dom 𝐺 )
14 13 9 eqeq12d ⊢ ( 𝑙 = 𝐾 → ( dom ( glb ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ↔ dom 𝐺 = 𝒫 𝐵 ) )
15 10 14 anbi12d ⊢ ( 𝑙 = 𝐾 → ( ( dom ( lub ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ∧ dom ( glb ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ) ↔ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )
16 df-clat ⊢ CLat = { 𝑙 ∈ Poset ∣ ( dom ( lub ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ∧ dom ( glb ‘ 𝑙 ) = 𝒫 ( Base ‘ 𝑙 ) ) }
17 15 16 elrab2 ⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom 𝑈 = 𝒫 𝐵 ∧ dom 𝐺 = 𝒫 𝐵 ) ) )