Theorem hashxnn0

Description: The value of the hash function for a set is an extended nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 10-Dec-2020)

	Ref	Expression
Assertion	hashxnn0	|- ( M e. V -> ( # ` M ) e. NN0* )

Proof

Step	Hyp	Ref	Expression
1		hashfxnn0	|- # : _V --> NN0*
2	1	a1i	|- ( M e. V -> # : _V --> NN0* )
3		elex	|- ( M e. V -> M e. _V )
4	2 3	ffvelrnd	|- ( M e. V -> ( # ` M ) e. NN0* )