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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccla	⊢ CLat
1		vp	⊢ 𝑝
2		cpo	⊢ Poset
3		club	⊢ lub
4	1	cv	⊢ 𝑝
5	4 3	cfv	⊢ ( lub ‘ 𝑝 )
6	5	cdm	⊢ dom ( lub ‘ 𝑝 )
7		cbs	⊢ Base
8	4 7	cfv	⊢ ( Base ‘ 𝑝 )
9	8	cpw	⊢ 𝒫 ( Base ‘ 𝑝 )
10	6 9	wceq	⊢ dom ( lub ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 )
11		cglb	⊢ glb
12	4 11	cfv	⊢ ( glb ‘ 𝑝 )
13	12	cdm	⊢ dom ( glb ‘ 𝑝 )
14	13 9	wceq	⊢ dom ( glb ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 )
15	10 14	wa	⊢ ( dom ( lub ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 ) ∧ dom ( glb ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 ) )
16	15 1 2	crab	⊢ { 𝑝 ∈ Poset ∣ ( dom ( lub ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 ) ∧ dom ( glb ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 ) ) }
17	0 16	wceq	⊢ CLat = { 𝑝 ∈ Poset ∣ ( dom ( lub ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 ) ∧ dom ( glb ‘ 𝑝 ) = 𝒫 ( Base ‘ 𝑝 ) ) }