Definition df-p0

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

	Ref	Expression
Assertion	df-p0	$$⊢\mathrm{0.}=\left(p\in \mathrm{V}⟼\mathrm{glb}\left(p\right)\left({\mathrm{Base}}_p\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cp0	$$class\mathrm{0.}$$
1		vp	$$setvarp$$
2		cvv	$$class\mathrm{V}$$
3		cglb	$$class\mathrm{glb}$$
4	1	cv	$$setvarp$$
5	4 3	cfv	$$class\mathrm{glb}\left(p\right)$$
6		cbs	$$class\mathrm{Base}$$
7	4 6	cfv	$$class{\mathrm{Base}}_p$$
8	7 5	cfv	$$class\mathrm{glb}\left(p\right)\left({\mathrm{Base}}_p\right)$$
9	1 2 8	cmpt	$$class\left(p\in \mathrm{V}⟼\mathrm{glb}\left(p\right)\left({\mathrm{Base}}_p\right)\right)$$
10	0 9	wceq	$$wff\mathrm{0.}=\left(p\in \mathrm{V}⟼\mathrm{glb}\left(p\right)\left({\mathrm{Base}}_p\right)\right)$$