Definition df-clat 18132

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 = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}

Detailed syntax breakdown of Definition df-clat

Step	Hyp	Ref	Expression
1		ccla 18131	. 2 class CLat
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1538	. . . . . . 7 class 𝑝
4		club 17942	. . . . . . 7 class lub
5	3, 4	cfv 6418	. . . . . 6 class (lub‘𝑝)
6	5	cdm 5580	. . . . 5 class dom (lub‘𝑝)
7		cbs 16840	. . . . . . 7 class Base
8	3, 7	cfv 6418	. . . . . 6 class (Base‘𝑝)
9	8	cpw 4530	. . . . 5 class 𝒫 (Base‘𝑝)
10	6, 9	wceq 1539	. . . 4 wff dom (lub‘𝑝) = 𝒫 (Base‘𝑝)
11		cglb 17943	. . . . . . 7 class glb
12	3, 11	cfv 6418	. . . . . 6 class (glb‘𝑝)
13	12	cdm 5580	. . . . 5 class dom (glb‘𝑝)
14	13, 9	wceq 1539	. . . 4 wff dom (glb‘𝑝) = 𝒫 (Base‘𝑝)
15	10, 14	wa 395	. . 3 wff (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))
16		cpo 17940	. . 3 class Poset
17	15, 2, 16	crab 3067	. 2 class {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}
18	1, 17	wceq 1539	1 wff CLat = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}

This definition is referenced by:  isclat  18133