Definition df-join 17981

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 17944	. 2 class join
2		vp	. . 3 setvar 𝑝
3		cvv 3422	. . 3 class V
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1538	. . . . . 6 class 𝑥
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1538	. . . . . 6 class 𝑦
8	5, 7	cpr 4560	. . . . 5 class {𝑥, 𝑦}
9		vz	. . . . . 6 setvar 𝑧
10	9	cv 1538	. . . . 5 class 𝑧
11	2	cv 1538	. . . . . 6 class 𝑝
12		club 17942	. . . . . 6 class lub
13	11, 12	cfv 6418	. . . . 5 class (lub‘𝑝)
14	8, 10, 13	wbr 5070	. . . 4 wff {𝑥, 𝑦} (lub‘𝑝)𝑧
15	14, 4, 6, 9	coprab 7256	. . 3 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧}
16	2, 3, 15	cmpt 5153	. 2 class (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})
17	1, 16	wceq 1539	1 wff join = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (lub‘𝑝)𝑧})

This definition is referenced by:  joinfval  18006