Metamath Proof Explorer


Theorem mzpval

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

Ref Expression
Assertion mzpval ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) = ( mzPolyCld ‘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 mzpcln0 ( 𝑉 ∈ V → ( mzPolyCld ‘ 𝑉 ) ≠ ∅ )
2 intex ( ( mzPolyCld ‘ 𝑉 ) ≠ ∅ ↔ ( mzPolyCld ‘ 𝑉 ) ∈ V )
3 1 2 sylib ( 𝑉 ∈ V → ( mzPolyCld ‘ 𝑉 ) ∈ V )
4 fveq2 ( 𝑣 = 𝑉 → ( mzPolyCld ‘ 𝑣 ) = ( mzPolyCld ‘ 𝑉 ) )
5 4 inteqd ( 𝑣 = 𝑉 ( mzPolyCld ‘ 𝑣 ) = ( mzPolyCld ‘ 𝑉 ) )
6 df-mzp mzPoly = ( 𝑣 ∈ V ↦ ( mzPolyCld ‘ 𝑣 ) )
7 5 6 fvmptg ( ( 𝑉 ∈ V ∧ ( mzPolyCld ‘ 𝑉 ) ∈ V ) → ( mzPoly ‘ 𝑉 ) = ( mzPolyCld ‘ 𝑉 ) )
8 3 7 mpdan ( 𝑉 ∈ V → ( mzPoly ‘ 𝑉 ) = ( mzPolyCld ‘ 𝑉 ) )