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 = ( 𝑝 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cjn	⊢ join
1		vp	⊢ 𝑝
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5		vz	⊢ 𝑧
6	3	cv	⊢ 𝑥
7	4	cv	⊢ 𝑦
8	6 7	cpr	⊢ { 𝑥 , 𝑦 }
9		club	⊢ lub
10	1	cv	⊢ 𝑝
11	10 9	cfv	⊢ ( lub ‘ 𝑝 )
12	5	cv	⊢ 𝑧
13	8 12 11	wbr	⊢ { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧
14	13 3 4 5	coprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧 }
15	1 2 14	cmpt	⊢ ( 𝑝 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧 } )
16	0 15	wceq	⊢ join = ( 𝑝 ∈ V ↦ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ { 𝑥 , 𝑦 } ( lub ‘ 𝑝 ) 𝑧 } )