Definition df-clat 15940

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.)

Assertion

Ref	Expression
df-clat	|- CLat = { p e. Poset | ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) ) }

Detailed syntax breakdown of Definition df-clat

Step	Hyp	Ref	Expression
1		ccla 15939	. 2 class CLat
2		vp	. . . . . . . 8 setvar p
3	2	cv 1397	. . . . . . 7 class p
4		club 15773	. . . . . . 7 class lub
5	3, 4	cfv 5570	. . . . . 6 class ( lub ` p )
6	5	cdm 4988	. . . . 5 class dom ( lub ` p )
7		cbs 14719	. . . . . . 7 class Base
8	3, 7	cfv 5570	. . . . . 6 class ( Base ` p )
9	8	cpw 3999	. . . . 5 class ~P ( Base ` p )
10	6, 9	wceq 1398	. . . 4 wff dom ( lub ` p ) = ~P ( Base ` p )
11		cglb 15774	. . . . . . 7 class glb
12	3, 11	cfv 5570	. . . . . 6 class ( glb ` p )
13	12	cdm 4988	. . . . 5 class dom ( glb ` p )
14	13, 9	wceq 1398	. . . 4 wff dom ( glb ` p ) = ~P ( Base ` p )
15	10, 14	wa 367	. . 3 wff ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) )
16		cpo 15771	. . 3 class Poset
17	15, 2, 16	crab 2808	. 2 class { p e. Poset | ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) ) }
18	1, 17	wceq 1398	1 wff CLat = { p e. Poset | ( dom ( lub ` p ) = ~P ( Base ` p ) /\ dom ( glb ` p ) = ~P ( Base ` p ) ) }

This definition is referenced by:  isclat  15941