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