Theorem mzpval

Description: Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	mzpval	$$⊢V\in \mathrm{V}\to \mathrm{mzPoly}\left(V\right)=\bigcap \mathrm{mzPolyCld}\left(V\right)$$

Proof

Step	Hyp	Ref	Expression
1		mzpcln0	$$⊢V\in \mathrm{V}\to \mathrm{mzPolyCld}\left(V\right)\ne \varnothing$$
2		intex	$$⊢\mathrm{mzPolyCld}\left(V\right)\ne \varnothing \leftrightarrow \bigcap \mathrm{mzPolyCld}\left(V\right)\in \mathrm{V}$$
3	1 2	sylib	$$⊢V\in \mathrm{V}\to \bigcap \mathrm{mzPolyCld}\left(V\right)\in \mathrm{V}$$
4		fveq2	$$⊢v=V\to \mathrm{mzPolyCld}\left(v\right)=\mathrm{mzPolyCld}\left(V\right)$$
5	4	inteqd	$$⊢v=V\to \bigcap \mathrm{mzPolyCld}\left(v\right)=\bigcap \mathrm{mzPolyCld}\left(V\right)$$
6		df-mzp	$$⊢\mathrm{mzPoly}=\left(v\in \mathrm{V}⟼\bigcap \mathrm{mzPolyCld}\left(v\right)\right)$$
7	5 6	fvmptg	$$⊢\left(V\in \mathrm{V}\wedge \bigcap \mathrm{mzPolyCld}\left(V\right)\in \mathrm{V}\right)\to \mathrm{mzPoly}\left(V\right)=\bigcap \mathrm{mzPolyCld}\left(V\right)$$
8	3 7	mpdan	$$⊢V\in \mathrm{V}\to \mathrm{mzPoly}\left(V\right)=\bigcap \mathrm{mzPolyCld}\left(V\right)$$