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 ↦ ∩ ( mzPolyCld ‘ 𝑣 ) )
2	1	dmeqi	⊢ dom mzPoly = dom ( 𝑣 ∈ V ↦ ∩ ( mzPolyCld ‘ 𝑣 ) )
3		dmmptg	⊢ ( ∀ 𝑣 ∈ V ∩ ( mzPolyCld ‘ 𝑣 ) ∈ V → dom ( 𝑣 ∈ V ↦ ∩ ( mzPolyCld ‘ 𝑣 ) ) = V )
4		mzpcln0	⊢ ( 𝑣 ∈ V → ( mzPolyCld ‘ 𝑣 ) ≠ ∅ )
5		intex	⊢ ( ( mzPolyCld ‘ 𝑣 ) ≠ ∅ ↔ ∩ ( mzPolyCld ‘ 𝑣 ) ∈ V )
6	4 5	sylib	⊢ ( 𝑣 ∈ V → ∩ ( mzPolyCld ‘ 𝑣 ) ∈ V )
7	3 6	mprg	⊢ dom ( 𝑣 ∈ V ↦ ∩ ( mzPolyCld ‘ 𝑣 ) ) = V
8	2 7	eqtri	⊢ dom mzPoly = V