Definition df-p0 16862

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

Assertion

Ref	Expression
df-p0	⊢ 0. = (𝑝 ∈ V ↦ ((glb‘𝑝)‘(Base‘𝑝)))

Detailed syntax breakdown of Definition df-p0

Step	Hyp	Ref	Expression
1		cp0 16860	. 2 class 0.
2		vp	. . 3 setvar 𝑝
3		cvv 3173	. . 3 class V
4	2	cv 1474	. . . . 5 class 𝑝
5		cbs 15695	. . . . 5 class Base
6	4, 5	cfv 5804	. . . 4 class (Base‘𝑝)
7		cglb 16766	. . . . 5 class glb
8	4, 7	cfv 5804	. . . 4 class (glb‘𝑝)
9	6, 8	cfv 5804	. . 3 class ((glb‘𝑝)‘(Base‘𝑝))
10	2, 3, 9	cmpt 4643	. 2 class (𝑝 ∈ V ↦ ((glb‘𝑝)‘(Base‘𝑝)))
11	1, 10	wceq 1475	1 wff 0. = (𝑝 ∈ V ↦ ((glb‘𝑝)‘(Base‘𝑝)))

This definition is referenced by:  p0val  16864