Definition df-lat 17046

Description: Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)

Assertion

Ref	Expression
df-lat	|- Lat = { p e. Poset | ( dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) /\ dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) ) }

Detailed syntax breakdown of Definition df-lat

Step	Hyp	Ref	Expression
1		clat 17045	. 2 class Lat
2		vp	. . . . . . . 8 setvar p
3	2	cv 1482	. . . . . . 7 class p
4		cjn 16944	. . . . . . 7 class join
5	3, 4	cfv 5888	. . . . . 6 class ( join ` p )
6	5	cdm 5114	. . . . 5 class dom ( join ` p )
7		cbs 15857	. . . . . . 7 class Base
8	3, 7	cfv 5888	. . . . . 6 class ( Base ` p )
9	8, 8	cxp 5112	. . . . 5 class ( ( Base ` p ) X. ( Base ` p ) )
10	6, 9	wceq 1483	. . . 4 wff dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) )
11		cmee 16945	. . . . . . 7 class meet
12	3, 11	cfv 5888	. . . . . 6 class ( meet ` p )
13	12	cdm 5114	. . . . 5 class dom ( meet ` p )
14	13, 9	wceq 1483	. . . 4 wff dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) )
15	10, 14	wa 384	. . 3 wff ( dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) /\ dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) )
16		cpo 16940	. . 3 class Poset
17	15, 2, 16	crab 2916	. 2 class { p e. Poset | ( dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) /\ dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) ) }
18	1, 17	wceq 1483	1 wff Lat = { p e. Poset | ( dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) /\ dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) ) }

This definition is referenced by:  islat  17047