# 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 ${⊢}{B}={\mathrm{Base}}_{{K}}$
isclat.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
isclat.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
Assertion isclat ${⊢}{K}\in \mathrm{CLat}↔\left({K}\in \mathrm{Poset}\wedge \left(\mathrm{dom}{U}=𝒫{B}\wedge \mathrm{dom}{G}=𝒫{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 isclat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 isclat.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
3 isclat.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
4 fveq2 ${⊢}{l}={K}\to \mathrm{lub}\left({l}\right)=\mathrm{lub}\left({K}\right)$
5 4 2 eqtr4di ${⊢}{l}={K}\to \mathrm{lub}\left({l}\right)={U}$
6 5 dmeqd ${⊢}{l}={K}\to \mathrm{dom}\mathrm{lub}\left({l}\right)=\mathrm{dom}{U}$
7 fveq2 ${⊢}{l}={K}\to {\mathrm{Base}}_{{l}}={\mathrm{Base}}_{{K}}$
8 7 1 eqtr4di ${⊢}{l}={K}\to {\mathrm{Base}}_{{l}}={B}$
9 8 pweqd ${⊢}{l}={K}\to 𝒫{\mathrm{Base}}_{{l}}=𝒫{B}$
10 6 9 eqeq12d ${⊢}{l}={K}\to \left(\mathrm{dom}\mathrm{lub}\left({l}\right)=𝒫{\mathrm{Base}}_{{l}}↔\mathrm{dom}{U}=𝒫{B}\right)$
11 fveq2 ${⊢}{l}={K}\to \mathrm{glb}\left({l}\right)=\mathrm{glb}\left({K}\right)$
12 11 3 eqtr4di ${⊢}{l}={K}\to \mathrm{glb}\left({l}\right)={G}$
13 12 dmeqd ${⊢}{l}={K}\to \mathrm{dom}\mathrm{glb}\left({l}\right)=\mathrm{dom}{G}$
14 13 9 eqeq12d ${⊢}{l}={K}\to \left(\mathrm{dom}\mathrm{glb}\left({l}\right)=𝒫{\mathrm{Base}}_{{l}}↔\mathrm{dom}{G}=𝒫{B}\right)$
15 10 14 anbi12d ${⊢}{l}={K}\to \left(\left(\mathrm{dom}\mathrm{lub}\left({l}\right)=𝒫{\mathrm{Base}}_{{l}}\wedge \mathrm{dom}\mathrm{glb}\left({l}\right)=𝒫{\mathrm{Base}}_{{l}}\right)↔\left(\mathrm{dom}{U}=𝒫{B}\wedge \mathrm{dom}{G}=𝒫{B}\right)\right)$
16 df-clat ${⊢}\mathrm{CLat}=\left\{{l}\in \mathrm{Poset}|\left(\mathrm{dom}\mathrm{lub}\left({l}\right)=𝒫{\mathrm{Base}}_{{l}}\wedge \mathrm{dom}\mathrm{glb}\left({l}\right)=𝒫{\mathrm{Base}}_{{l}}\right)\right\}$
17 15 16 elrab2 ${⊢}{K}\in \mathrm{CLat}↔\left({K}\in \mathrm{Poset}\wedge \left(\mathrm{dom}{U}=𝒫{B}\wedge \mathrm{dom}{G}=𝒫{B}\right)\right)$