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	$$⊢\mathrm{Lat}=\left\{p\in \mathrm{Poset}|\left(\mathrm{dom}\mathrm{join}\left(p\right)={\mathrm{Base}}_p\times {\mathrm{Base}}_p\wedge \mathrm{dom}\mathrm{meet}\left(p\right)={\mathrm{Base}}_p\times {\mathrm{Base}}_p\right)\right\}$$

Detailed syntax breakdown

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