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 e. _V |-> |^| ( mzPolyCld ` v ) )
2	1	dmeqi	|- dom mzPoly = dom ( v e. _V |-> |^| ( mzPolyCld ` v ) )
3		dmmptg	|- ( A. v e. _V |^| ( mzPolyCld ` v ) e. _V -> dom ( v e. _V |-> |^| ( mzPolyCld ` v ) ) = _V )
4		mzpcln0	|- ( v e. _V -> ( mzPolyCld ` v ) =/= (/) )
5		intex	|- ( ( mzPolyCld ` v ) =/= (/) <-> |^| ( mzPolyCld ` v ) e. _V )
6	4 5	sylib	|- ( v e. _V -> |^| ( mzPolyCld ` v ) e. _V )
7	3 6	mprg	|- dom ( v e. _V |-> |^| ( mzPolyCld ` v ) ) = _V
8	2 7	eqtri	|- dom mzPoly = _V