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 e. _V -> ( mzPolyCld ` V ) =/= (/) )

Proof

Step Hyp Ref Expression
1 mzpclall 
 |-  ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. ( mzPolyCld ` V ) )
2 1 ne0d 
 |-  ( V e. _V -> ( mzPolyCld ` V ) =/= (/) )