Definition df-join 17586

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

Assertion

Ref	Expression
df-join	⊢ join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})

Distinct variable group:   𝑥,𝑝,𝑦,𝑧

Detailed syntax breakdown of Definition df-join

Step	Hyp	Ref	Expression
1		cjn 17554	. 2 class join
2		vp	. . 3 setvar 𝑝
3		cvv 3494	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1536	. . . . . 6 class 𝑥
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1536	. . . . . 6 class 𝑦
8	5, 7	cpr 4569	. . . . 5 class {𝑥, 𝑦}
9		vz	. . . . . 6 setvar 𝑧
10	9	cv 1536	. . . . 5 class 𝑧
11	2	cv 1536	. . . . . 6 class 𝑝
12		club 17552	. . . . . 6 class lub
13	11, 12	cfv 6355	. . . . 5 class (lub‘𝑝)
14	8, 10, 13	wbr 5066	. . . 4 wff {𝑥, 𝑦} (lub‘𝑝)𝑧
15	14, 4, 6, 9	coprab 7157	. . 3 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧}
16	2, 3, 15	cmpt 5146	. 2 class (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})
17	1, 16	wceq 1537	1 wff join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})

This definition is referenced by:  joinfval  17611