Theorem mzpcln0

Description: Corollary of mzpclall : polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Assertion	mzpcln0	⊢ ( 𝑉 ∈ V → ( mzPolyCld ‘ 𝑉 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		mzpclall	⊢ ( 𝑉 ∈ V → ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ ( mzPolyCld ‘ 𝑉 ) )
2	1	ne0d	⊢ ( 𝑉 ∈ V → ( mzPolyCld ‘ 𝑉 ) ≠ ∅ )