df-meet

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

		Ref	Expression
	Assertion	df-meet	$⊢ meet = (p \in V ⟼ \{⟨⟨x, y⟩, z⟩ \| \{x, y\} glb (p) z\})$

Step	Hyp	Ref	Expression
0		cmee	$class meet$
1		vp	$setvar p$
2		cvv	$class V$
3		vx	$setvar x$
4		vy	$setvar y$
5		vz	$setvar z$
6	3	cv	$setvar x$
7	4	cv	$setvar y$
8	6 7	cpr	$class \{x, y\}$
9		cglb	$class glb$
10	1	cv	$setvar p$
11	10 9	cfv	$class glb (p)$
12	5	cv	$setvar z$
13	8 12 11	wbr	$wff \{x, y\} glb (p) z$
14	13 3 4 5	coprab	$class \{⟨⟨x, y⟩, z⟩ \| \{x, y\} glb (p) z\}$
15	1 2 14	cmpt	$class (p \in V ⟼ \{⟨⟨x, y⟩, z⟩ \| \{x, y\} glb (p) z\})$
16	0 15	wceq	$wff meet = (p \in V ⟼ \{⟨⟨x, y⟩, z⟩ \| \{x, y\} glb (p) z\})$

Metamath Proof Explorer