Definition df-p0

Description: Define poset zero. (Contributed by NM, 12-Oct-2011)

	Ref	Expression
Assertion	df-p0	|- 0. = ( p e. _V |-> ( ( glb ` p ) ` ( Base ` p ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cp0	|- 0.
1		vp	|- p
2		cvv	|- _V
3		cglb	|- glb
4	1	cv	|- p
5	4 3	cfv	|- ( glb ` p )
6		cbs	|- Base
7	4 6	cfv	|- ( Base ` p )
8	7 5	cfv	|- ( ( glb ` p ) ` ( Base ` p ) )
9	1 2 8	cmpt	|- ( p e. _V |-> ( ( glb ` p ) ` ( Base ` p ) ) )
10	0 9	wceq	|- 0. = ( p e. _V |-> ( ( glb ` p ) ` ( Base ` p ) ) )