Definition df-p0

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cp0	⊢ 0.
1		vp	⊢ 𝑝
2		cvv	⊢ V
3		cglb	⊢ glb
4	1	cv	⊢ 𝑝
5	4 3	cfv	⊢ ( glb ‘ 𝑝 )
6		cbs	⊢ Base
7	4 6	cfv	⊢ ( Base ‘ 𝑝 )
8	7 5	cfv	⊢ ( ( glb ‘ 𝑝 ) ‘ ( Base ‘ 𝑝 ) )
9	1 2 8	cmpt	⊢ ( 𝑝 ∈ V ↦ ( ( glb ‘ 𝑝 ) ‘ ( Base ‘ 𝑝 ) ) )
10	0 9	wceq	⊢ 0. = ( 𝑝 ∈ V ↦ ( ( glb ‘ 𝑝 ) ‘ ( Base ‘ 𝑝 ) ) )