Definition df-meet

Description: Define poset meet. (Contributed by NM, 12-Sep-2011) (Revised by NM, 8-Sep-2018)

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

Detailed syntax breakdown

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