Definition df-meet

Description: Define poset meet. (Contributed by NM, 12-Sep-2011) (Revised by NM, 8-Sep-2018)

	Ref	Expression
Assertion	df-meet	$$⊢\mathrm{meet}=\left(p\in \mathrm{V}⟼\left\{⟨⟨x,y⟩,z⟩|\left\{x,y\right\}\mathrm{glb}\left(p\right)z\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmee	$$class\mathrm{meet}$$
1		vp	$$setvarp$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		vy	$$setvary$$
5		vz	$$setvarz$$
6	3	cv	$$setvarx$$
7	4	cv	$$setvary$$
8	6 7	cpr	$$class\left\{x,y\right\}$$
9		cglb	$$class\mathrm{glb}$$
10	1	cv	$$setvarp$$
11	10 9	cfv	$$class\mathrm{glb}\left(p\right)$$
12	5	cv	$$setvarz$$
13	8 12 11	wbr	$$wff\left\{x,y\right\}\mathrm{glb}\left(p\right)z$$
14	13 3 4 5	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|\left\{x,y\right\}\mathrm{glb}\left(p\right)z\right\}$$
15	1 2 14	cmpt	$$class\left(p\in \mathrm{V}⟼\left\{⟨⟨x,y⟩,z⟩|\left\{x,y\right\}\mathrm{glb}\left(p\right)z\right\}\right)$$
16	0 15	wceq	$$wff\mathrm{meet}=\left(p\in \mathrm{V}⟼\left\{⟨⟨x,y⟩,z⟩|\left\{x,y\right\}\mathrm{glb}\left(p\right)z\right\}\right)$$