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	$$setvarp$$
2		cpo	$$class\mathrm{Poset}$$
3		club	$$class\mathrm{lub}$$
4	1	cv	$$setvarp$$
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\}$$