Metamath Proof Explorer

Theorem mzpval

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

Ref Expression
Assertion mzpval ⊢ V ∈ V → mzPoly ⁡ V = ⋂ mzPolyCld ⁡ V

Proof

Step Hyp Ref Expression
1 mzpcln0 ⊢ V ∈ V → mzPolyCld ⁡ V ≠ ∅
2 intex ⊢ mzPolyCld ⁡ V ≠ ∅ ↔ ⋂ mzPolyCld ⁡ V ∈ V
3 1 2 sylib ⊢ V ∈ V → ⋂ mzPolyCld ⁡ V ∈ V
4 fveq2 ⊢ v = V → mzPolyCld ⁡ v = mzPolyCld ⁡ V
5 4 inteqd ⊢ v = V → ⋂ mzPolyCld ⁡ v = ⋂ mzPolyCld ⁡ V
6 df-mzp ⊢ mzPoly = v ∈ V ⟼ ⋂ mzPolyCld ⁡ v
7 5 6 fvmptg ⊢ V ∈ V ∧ ⋂ mzPolyCld ⁡ V ∈ V → mzPoly ⁡ V = ⋂ mzPolyCld ⁡ V
8 3 7 mpdan ⊢ V ∈ V → mzPoly ⁡ V = ⋂ mzPolyCld ⁡ V