Definition df-clat 18544

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 18543	. 2 class CLat
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1539	. . . . . . 7 class 𝑝
4		club 18355	. . . . . . 7 class lub
5	3, 4	cfv 6561	. . . . . 6 class (lub‘𝑝)
6	5	cdm 5685	. . . . 5 class dom (lub‘𝑝)
7		cbs 17247	. . . . . . 7 class Base
8	3, 7	cfv 6561	. . . . . 6 class (Base‘𝑝)
9	8	cpw 4600	. . . . 5 class 𝒫 (Base‘𝑝)
10	6, 9	wceq 1540	. . . 4 wff dom (lub‘𝑝) = 𝒫 (Base‘𝑝)
11		cglb 18356	. . . . . . 7 class glb
12	3, 11	cfv 6561	. . . . . 6 class (glb‘𝑝)
13	12	cdm 5685	. . . . 5 class dom (glb‘𝑝)
14	13, 9	wceq 1540	. . . 4 wff dom (glb‘𝑝) = 𝒫 (Base‘𝑝)
15	10, 14	wa 395	. . 3 wff (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))
16		cpo 18353	. . 3 class Poset
17	15, 2, 16	crab 3436	. 2 class {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}
18	1, 17	wceq 1540	1 wff CLat = {𝑝 ∈ Poset ∣ (dom (lub‘𝑝) = 𝒫 (Base‘𝑝) ∧ dom (glb‘𝑝) = 𝒫 (Base‘𝑝))}

This definition is referenced by:  isclat  18545