# Metamath Proof Explorer

## Definition df-clat

Description: Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012) (Revised by NM, 12-Sep-2018)

Ref Expression
Assertion df-clat ${⊢}\mathrm{CLat}=\left\{{p}\in \mathrm{Poset}|\left(\mathrm{dom}\mathrm{lub}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\wedge \mathrm{dom}\mathrm{glb}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 ccla ${class}\mathrm{CLat}$
1 vp ${setvar}{p}$
2 cpo ${class}\mathrm{Poset}$
3 club ${class}\mathrm{lub}$
4 1 cv ${setvar}{p}$
5 4 3 cfv ${class}\mathrm{lub}\left({p}\right)$
6 5 cdm ${class}\mathrm{dom}\mathrm{lub}\left({p}\right)$
7 cbs ${class}\mathrm{Base}$
8 4 7 cfv ${class}{\mathrm{Base}}_{{p}}$
9 8 cpw ${class}𝒫{\mathrm{Base}}_{{p}}$
10 6 9 wceq ${wff}\mathrm{dom}\mathrm{lub}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}$
11 cglb ${class}\mathrm{glb}$
12 4 11 cfv ${class}\mathrm{glb}\left({p}\right)$
13 12 cdm ${class}\mathrm{dom}\mathrm{glb}\left({p}\right)$
14 13 9 wceq ${wff}\mathrm{dom}\mathrm{glb}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}$
15 10 14 wa ${wff}\left(\mathrm{dom}\mathrm{lub}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\wedge \mathrm{dom}\mathrm{glb}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\right)$
16 15 1 2 crab ${class}\left\{{p}\in \mathrm{Poset}|\left(\mathrm{dom}\mathrm{lub}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\wedge \mathrm{dom}\mathrm{glb}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\right)\right\}$
17 0 16 wceq ${wff}\mathrm{CLat}=\left\{{p}\in \mathrm{Poset}|\left(\mathrm{dom}\mathrm{lub}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\wedge \mathrm{dom}\mathrm{glb}\left({p}\right)=𝒫{\mathrm{Base}}_{{p}}\right)\right\}$