Definition df-join

Description: Define poset join. (Contributed by NM, 12-Sep-2011) (Revised by Mario Carneiro, 3-Nov-2015)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cjn	|- join
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		club	|- lub
10	1	cv	|- p
11	10 9	cfv	|- ( lub ` p )
12	5	cv	|- z
13	8 12 11	wbr	|- { x , y } ( lub ` p ) z
14	13 3 4 5	coprab	|- { <. <. x , y >. , z >. | { x , y } ( lub ` p ) z }
15	1 2 14	cmpt	|- ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( lub ` p ) z } )
16	0 15	wceq	|- join = ( p e. _V |-> { <. <. x , y >. , z >. | { x , y } ( lub ` p ) z } )