Definition df-meet 16977

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

Assertion

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

Distinct variable group:   x, p, y, z

Detailed syntax breakdown of Definition df-meet

Step	Hyp	Ref	Expression
1		cmee 16945	. 2 class meet
2		vp	. . 3 setvar p
3		cvv 3200	. . 3 class _V
4		vx	. . . . . . 7 setvar x
5	4	cv 1482	. . . . . 6 class x
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8	5, 7	cpr 4179	. . . . 5 class { x , y }
9		vz	. . . . . 6 setvar z
10	9	cv 1482	. . . . 5 class z
11	2	cv 1482	. . . . . 6 class p
12		cglb 16943	. . . . . 6 class glb
13	11, 12	cfv 5888	. . . . 5 class ( glb ` p )
14	8, 10, 13	wbr 4653	. . . 4 wff { x , y } ( glb ` p ) z
15	14, 4, 6, 9	coprab 6651	. . 3 class { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z }
16	2, 3, 15	cmpt 4729	. 2 class ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z } )
17	1, 16	wceq 1483	1 wff meet = ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( glb ` p ) z } )

This definition is referenced by:  meetfval  17015