Theorem hashnn0pnf

Description: The value of the hash function for a set is either a nonnegative integer or positive infinity. TODO-AV: mark as OBSOLETE and replace it by hashxnn0 ? (Contributed by Alexander van der Vekens, 6-Dec-2017)

	Ref	Expression
Assertion	hashnn0pnf	|- ( M e. V -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) )

Proof

Step	Hyp	Ref	Expression
1		hashf	|- # : _V --> ( NN0 u. { +oo } )
2	1	a1i	|- ( M e. V -> # : _V --> ( NN0 u. { +oo } ) )
3		elex	|- ( M e. V -> M e. _V )
4	2 3	ffvelcdmd	|- ( M e. V -> ( # ` M ) e. ( NN0 u. { +oo } ) )
5		elun	|- ( ( # ` M ) e. ( NN0 u. { +oo } ) <-> ( ( # ` M ) e. NN0 \/ ( # ` M ) e. { +oo } ) )
6		elsni	|- ( ( # ` M ) e. { +oo } -> ( # ` M ) = +oo )
7	6	orim2i	|- ( ( ( # ` M ) e. NN0 \/ ( # ` M ) e. { +oo } ) -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) )
8	5 7	sylbi	|- ( ( # ` M ) e. ( NN0 u. { +oo } ) -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) )
9	4 8	syl	|- ( M e. V -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) )