Theorem p0val

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

	Ref	Expression
Hypotheses	p0val.b	$$⊢B={\mathrm{Base}}_K$$
	p0val.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	p0val.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
Assertion	p0val	$$⊢K\in V\to \underset{\dot{}}{0}=G\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		p0val.b	$$⊢B={\mathrm{Base}}_K$$
2		p0val.g	$$⊢G=\mathrm{glb}\left(K\right)$$
3		p0val.z	$$⊢\underset{\dot{}}{0}=\mathrm{0.}\left(K\right)$$
4		elex	$$⊢K\in V\to K\in \mathrm{V}$$
5		fveq2	$$⊢p=K\to \mathrm{glb}\left(p\right)=\mathrm{glb}\left(K\right)$$
6	5 2	eqtr4di	$$⊢p=K\to \mathrm{glb}\left(p\right)=G$$
7		fveq2	$$⊢p=K\to {\mathrm{Base}}_p={\mathrm{Base}}_K$$
8	7 1	eqtr4di	$$⊢p=K\to {\mathrm{Base}}_p=B$$
9	6 8	fveq12d	$$⊢p=K\to \mathrm{glb}\left(p\right)\left({\mathrm{Base}}_p\right)=G\left(B\right)$$
10		df-p0	$$⊢\mathrm{0.}=\left(p\in \mathrm{V}⟼\mathrm{glb}\left(p\right)\left({\mathrm{Base}}_p\right)\right)$$
11		fvex	$$⊢G\left(B\right)\in \mathrm{V}$$
12	9 10 11	fvmpt	$$⊢K\in \mathrm{V}\to \mathrm{0.}\left(K\right)=G\left(B\right)$$
13	3 12	syl5eq	$$⊢K\in \mathrm{V}\to \underset{\dot{}}{0}=G\left(B\right)$$
14	4 13	syl	$$⊢K\in V\to \underset{\dot{}}{0}=G\left(B\right)$$