This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-p0

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

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

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