Definition df-meet 18076

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

Assertion

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

Distinct variable group:   𝑥,𝑝,𝑦,𝑧

Detailed syntax breakdown of Definition df-meet

Step	Hyp	Ref	Expression
1		cmee 18039	. 2 class meet
2		vp	. . 3 setvar 𝑝
3		cvv 3433	. . 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 4564	. . . . 5 class {𝑥, 𝑦}
9		vz	. . . . . 6 setvar 𝑧
10	9	cv 1538	. . . . 5 class 𝑧
11	2	cv 1538	. . . . . 6 class 𝑝
12		cglb 18037	. . . . . 6 class glb
13	11, 12	cfv 6437	. . . . 5 class (glb‘𝑝)
14	8, 10, 13	wbr 5075	. . . 4 wff {𝑥, 𝑦} (glb‘𝑝)𝑧
15	14, 4, 6, 9	coprab 7285	. . 3 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}
16	2, 3, 15	cmpt 5158	. 2 class (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
17	1, 16	wceq 1539	1 wff meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})

This definition is referenced by:  meetfval  18114