Metamath Proof Explorer


Theorem dmmzp

Description: mzPoly is defined for all index sets which are sets. This is used with elfvdm to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion dmmzp dom mzPoly = V

Proof

Step Hyp Ref Expression
1 df-mzp mzPoly = v V mzPolyCld v
2 1 dmeqi dom mzPoly = dom v V mzPolyCld v
3 dmmptg v V mzPolyCld v V dom v V mzPolyCld v = V
4 mzpcln0 v V mzPolyCld v
5 intex mzPolyCld v mzPolyCld v V
6 4 5 sylib v V mzPolyCld v V
7 3 6 mprg dom v V mzPolyCld v = V
8 2 7 eqtri dom mzPoly = V