Definition df-meet

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

	Ref	Expression
Assertion	df-meet	|- meet = ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmee	|- meet
1		vp	|- p
2		cvv	|- _V
3		vx	|- x
4		vy	|- y
5		vz	|- z
6	3	cv	|- x
7	4	cv	|- y
8	6 7	cpr	|- { x , y }
9		cglb	|- glb
10	1	cv	|- p
11	10 9	cfv	|- ( glb ` p )
12	5	cv	|- z
13	8 12 11	wbr	|- { x , y } ( glb ` p ) z
14	13 3 4 5	coprab	|- { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z }
15	1 2 14	cmpt	|- ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z } )
16	0 15	wceq	|- meet = ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z } )