Metamath Proof Explorer


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 ffvelrnd
 |-  ( 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 ) )