Definition df-lat

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)

	Ref	Expression
Assertion	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

Step	Hyp	Ref	Expression
0		clat	|- Lat
1		vp	|- p
2		cpo	|- Poset
3		cjn	|- join
4	1	cv	|- p
5	4 3	cfv	|- ( join ` p )
6	5	cdm	|- dom ( join ` p )
7		cbs	|- Base
8	4 7	cfv	|- ( Base ` p )
9	8 8	cxp	|- ( ( Base ` p ) X. ( Base ` p ) )
10	6 9	wceq	|- dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) )
11		cmee	|- meet
12	4 11	cfv	|- ( meet ` p )
13	12	cdm	|- dom ( meet ` p )
14	13 9	wceq	|- dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) )
15	10 14	wa	|- ( dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) /\ dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) )
16	15 1 2	crab	|- { p e. Poset | ( dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) /\ dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) ) }
17	0 16	wceq	|- Lat = { p e. Poset | ( dom ( join ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) /\ dom ( meet ` p ) = ( ( Base ` p ) X. ( Base ` p ) ) ) }