Theorem p1val

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

	Ref	Expression
Hypotheses	p1val.b	|- B = ( Base ` K )
	p1val.u	|- U = ( lub ` K )
	p1val.t	|- .1. = ( 1. ` K )
Assertion	p1val	|- ( K e. V -> .1. = ( U ` B ) )

Proof

Step	Hyp	Ref	Expression
1		p1val.b	|- B = ( Base ` K )
2		p1val.u	|- U = ( lub ` K )
3		p1val.t	|- .1. = ( 1. ` K )
4		elex	|- ( K e. V -> K e. _V )
5		fveq2	|- ( k = K -> ( lub ` k ) = ( lub ` K ) )
6	5 2	eqtr4di	|- ( k = K -> ( lub ` k ) = U )
7		fveq2	|- ( k = K -> ( Base ` k ) = ( Base ` K ) )
8	7 1	eqtr4di	|- ( k = K -> ( Base ` k ) = B )
9	6 8	fveq12d	|- ( k = K -> ( ( lub ` k ) ` ( Base ` k ) ) = ( U ` B ) )
10		df-p1	|- 1. = ( k e. _V |-> ( ( lub ` k ) ` ( Base ` k ) ) )
11		fvex	|- ( U ` B ) e. _V
12	9 10 11	fvmpt	|- ( K e. _V -> ( 1. ` K ) = ( U ` B ) )
13	3 12	syl5eq	|- ( K e. _V -> .1. = ( U ` B ) )
14	4 13	syl	|- ( K e. V -> .1. = ( U ` B ) )