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	|- CLat = { p e. Poset | ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccla	|- CLat
1		vp	|- p
2		cpo	|- Poset
3		club	|- lub
4	1	cv	|- p
5	4 3	cfv	|- ( lub ` p )
6	5	cdm	|- dom ( lub ` p )
7		cbs	|- Base
8	4 7	cfv	|- ( Base ` p )
9	8	cpw	|- ~P ( Base ` p )
10	6 9	wceq	|- dom ( lub ` p ) = ~P ( Base ` p )
11		cglb	|- glb
12	4 11	cfv	|- ( glb ` p )
13	12	cdm	|- dom ( glb ` p )
14	13 9	wceq	|- dom ( glb ` p ) = ~P ( Base ` p )
15	10 14	wa	|- ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) )
16	15 1 2	crab	|- { p e. Poset | ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) ) }
17	0 16	wceq	|- CLat = { p e. Poset | ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) ) }