Definition df-clat 14492

Description: Define the class of all complete lattices. (Contributed by NM, 18-Oct-2012.)

Assertion

Ref	Expression
df-clat	|- CLat = { p e. Poset | A. s ( s C_ ( Base ` p ) -> ( ( ( lub ` p ) ` s ) e. ( Base ` p ) /\ ( ( glb ` p ) ` s ) e. ( Base ` p ) ) ) }

Distinct variable group:   s, p

Detailed syntax breakdown of Definition df-clat

Step	Hyp	Ref	Expression
1		ccla 14491	. 2 class CLat
2		vs	. . . . . . 7 set s
3	2	cv 1648	. . . . . 6 class s
4		vp	. . . . . . . 8 set p
5	4	cv 1648	. . . . . . 7 class p
6		cbs 13424	. . . . . . 7 class Base
7	5, 6	cfv 5413	. . . . . 6 class ( Base ` p )
8	3, 7	wss 3280	. . . . 5 wff s C_ ( Base ` p )
9		club 14354	. . . . . . . . 9 class lub
10	5, 9	cfv 5413	. . . . . . . 8 class ( lub ` p )
11	3, 10	cfv 5413	. . . . . . 7 class ( ( lub ` p ) ` s )
12	11, 7	wcel 1721	. . . . . 6 wff ( ( lub ` p ) ` s ) e. ( Base ` p )
13		cglb 14355	. . . . . . . . 9 class glb
14	5, 13	cfv 5413	. . . . . . . 8 class ( glb ` p )
15	3, 14	cfv 5413	. . . . . . 7 class ( ( glb ` p ) ` s )
16	15, 7	wcel 1721	. . . . . 6 wff ( ( glb ` p ) ` s ) e. ( Base ` p )
17	12, 16	wa 359	. . . . 5 wff ( ( ( lub ` p ) ` s ) e. ( Base ` p ) /\ ( ( glb ` p ) ` s ) e. ( Base ` p ) )
18	8, 17	wi 4	. . . 4 wff ( s C_ ( Base ` p ) -> ( ( ( lub ` p ) ` s ) e. ( Base ` p ) /\ ( ( glb ` p ) ` s ) e. ( Base ` p ) ) )
19	18, 2	wal 1546	. . 3 wff A. s ( s C_ ( Base ` p ) -> ( ( ( lub ` p ) ` s ) e. ( Base ` p ) /\ ( ( glb ` p ) ` s ) e. ( Base ` p ) ) )
20		cpo 14352	. . 3 class Poset
21	19, 4, 20	crab 2670	. 2 class { p e. Poset | A. s ( s C_ ( Base ` p ) -> ( ( ( lub ` p ) ` s ) e. ( Base ` p ) /\ ( ( glb ` p ) ` s ) e. ( Base ` p ) ) ) }
22	1, 21	wceq 1649	1 wff CLat = { p e. Poset | A. s ( s C_ ( Base ` p ) -> ( ( ( lub ` p ) ` s ) e. ( Base ` p ) /\ ( ( glb ` p ) ` s ) e. ( Base ` p ) ) ) }

This definition is referenced by:  isclat  14493