Metamath Proof Explorer

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 \in Poset \| (dom join (p) = {Base}_{p} \times {Base}_{p} \land dom meet (p) = {Base}_{p} \times {Base}_{p})\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clat	$class Lat$
1		vp	$setvar p$
2		cpo	$class Poset$
3		cjn	$class join$
4	1	cv	$setvar p$
5	4 3	cfv	$class join (p)$
6	5	cdm	$class dom join (p)$
7		cbs	$class Base$
8	4 7	cfv	$class {Base}_{p}$
9	8 8	cxp	$class ({Base}_{p} \times {Base}_{p})$
10	6 9	wceq	$wff dom join (p) = {Base}_{p} \times {Base}_{p}$
11		cmee	$class meet$
12	4 11	cfv	$class meet (p)$
13	12	cdm	$class dom meet (p)$
14	13 9	wceq	$wff dom meet (p) = {Base}_{p} \times {Base}_{p}$
15	10 14	wa	$wff (dom join (p) = {Base}_{p} \times {Base}_{p} \land dom meet (p) = {Base}_{p} \times {Base}_{p})$
16	15 1 2	crab	$class \{p \in Poset \| (dom join (p) = {Base}_{p} \times {Base}_{p} \land dom meet (p) = {Base}_{p} \times {Base}_{p})\}$
17	0 16	wceq	$wff Lat = \{p \in Poset \| (dom join (p) = {Base}_{p} \times {Base}_{p} \land dom meet (p) = {Base}_{p} \times {Base}_{p})\}$