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	$$⊢\mathrm{join}=\left(p\in \mathrm{V}⟼\left\{⟨⟨x,y⟩,z⟩|\left\{x,y\right\}\mathrm{lub}\left(p\right)z\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cjn	$$class\mathrm{join}$$
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		club	$$class\mathrm{lub}$$
10	1	cv	$$setvarp$$
11	10 9	cfv	$$class\mathrm{lub}\left(p\right)$$
12	5	cv	$$setvarz$$
13	8 12 11	wbr	$$wff\left\{x,y\right\}\mathrm{lub}\left(p\right)z$$
14	13 3 4 5	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|\left\{x,y\right\}\mathrm{lub}\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{lub}\left(p\right)z\right\}\right)$$
16	0 15	wceq	$$wff\mathrm{join}=\left(p\in \mathrm{V}⟼\left\{⟨⟨x,y⟩,z⟩|\left\{x,y\right\}\mathrm{lub}\left(p\right)z\right\}\right)$$