Theorem p1val

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

	Ref	Expression
Hypotheses	p1val.b	$$⊢B={\mathrm{Base}}_K$$
	p1val.u	$$⊢U=\mathrm{lub}\left(K\right)$$
	p1val.t	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	p1val	$$⊢K\in V\to \underset{\dot{}}{1}=U\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		p1val.b	$$⊢B={\mathrm{Base}}_K$$
2		p1val.u	$$⊢U=\mathrm{lub}\left(K\right)$$
3		p1val.t	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
4		elex	$$⊢K\in V\to K\in \mathrm{V}$$
5		fveq2	$$⊢k=K\to \mathrm{lub}\left(k\right)=\mathrm{lub}\left(K\right)$$
6	5 2	syl6eqr	$$⊢k=K\to \mathrm{lub}\left(k\right)=U$$
7		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
8	7 1	syl6eqr	$$⊢k=K\to {\mathrm{Base}}_k=B$$
9	6 8	fveq12d	$$⊢k=K\to \mathrm{lub}\left(k\right)\left({\mathrm{Base}}_k\right)=U\left(B\right)$$
10		df-p1	$$⊢\mathrm{1.}=\left(k\in \mathrm{V}⟼\mathrm{lub}\left(k\right)\left({\mathrm{Base}}_k\right)\right)$$
11		fvex	$$⊢U\left(B\right)\in \mathrm{V}$$
12	9 10 11	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{1.}\left(K\right)=U\left(B\right)$$
13	3 12	syl5eq	$$⊢K\in \mathrm{V}\to \underset{\dot{}}{1}=U\left(B\right)$$
14	4 13	syl	$$⊢K\in V\to \underset{\dot{}}{1}=U\left(B\right)$$