# Metamath Proof Explorer

## 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 ${setvar}{p}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 vy ${setvar}{y}$
5 vz ${setvar}{z}$
6 3 cv ${setvar}{x}$
7 4 cv ${setvar}{y}$
8 6 7 cpr ${class}\left\{{x},{y}\right\}$
9 club ${class}\mathrm{lub}$
10 1 cv ${setvar}{p}$
11 10 9 cfv ${class}\mathrm{lub}\left({p}\right)$
12 5 cv ${setvar}{z}$
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)$