Theorem p0val

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

	Ref	Expression
Hypotheses	p0val.b	|- B = ( Base ` K )
	p0val.g	|- G = ( glb ` K )
	p0val.z	|- .0. = ( 0. ` K )
Assertion	p0val	|- ( K e. V -> .0. = ( G ` B ) )

Proof

Step	Hyp	Ref	Expression
1		p0val.b	|- B = ( Base ` K )
2		p0val.g	|- G = ( glb ` K )
3		p0val.z	|- .0. = ( 0. ` K )
4		elex	|- ( K e. V -> K e. _V )
5		fveq2	|- ( p = K -> ( glb ` p ) = ( glb ` K ) )
6	5 2	eqtr4di	|- ( p = K -> ( glb ` p ) = G )
7		fveq2	|- ( p = K -> ( Base ` p ) = ( Base ` K ) )
8	7 1	eqtr4di	|- ( p = K -> ( Base ` p ) = B )
9	6 8	fveq12d	|- ( p = K -> ( ( glb ` p ) ` ( Base ` p ) ) = ( G ` B ) )
10		df-p0	|- 0. = ( p e. _V |-> ( ( glb ` p ) ` ( Base ` p ) ) )
11		fvex	|- ( G ` B ) e. _V
12	9 10 11	fvmpt	|- ( K e. _V -> ( 0. ` K ) = ( G ` B ) )
13	3 12	syl5eq	|- ( K e. _V -> .0. = ( G ` B ) )
14	4 13	syl	|- ( K e. V -> .0. = ( G ` B ) )