Metamath Proof Explorer


Theorem mzpcln0

Description: Corrolary 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 ‘ 𝑉 ) ≠ ∅ )