Definition df-clat 18449

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 18448	. 2 class CLat
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1541	. . . . . . 7 class 𝑝
4		club 18259	. . . . . . 7 class lub
5	3, 4	cfv 6541	. . . . . 6 class (lub‘𝑝)
6	5	cdm 5676	. . . . 5 class dom (lub‘𝑝)
7		cbs 17141	. . . . . . 7 class Base
8	3, 7	cfv 6541	. . . . . 6 class (Base‘𝑝)
9	8	cpw 4602	. . . . 5 class 𝒫 (Base‘𝑝)
10	6, 9	wceq 1542	. . . 4 wff dom (lub‘𝑝) = 𝒫 (Base‘𝑝)
11		cglb 18260	. . . . . . 7 class glb
12	3, 11	cfv 6541	. . . . . 6 class (glb‘𝑝)
13	12	cdm 5676	. . . . 5 class dom (glb‘𝑝)
14	13, 9	wceq 1542	. . . 4 wff dom (glb‘𝑝) = 𝒫 (Base‘𝑝)
15	10, 14	wa 397	. . 3 wff (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))
16		cpo 18257	. . 3 class Poset
17	15, 2, 16	crab 3433	. 2 class {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}
18	1, 17	wceq 1542	1 wff CLat = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}

This definition is referenced by:  isclat  18450