This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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