Metamath Proof Explorer

Theorem hashfxnn0

Description: The size function is a function into the extended nonnegative integers. (Contributed by Mario Carneiro, 13-Sep-2013) (Revised by AV, 10-Dec-2020)

Ref Expression
Assertion hashfxnn0 
|- # : _V --> NN0*

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 eqid 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
3 1 2 hashkf 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) : Fin --> NN0
4 pnfex 
 |-  +oo e. _V
5 4 fconst 
 |-  ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo }
6 3 5 pm3.2i 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) : Fin --> NN0 /\ ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo } )
7 disjdif 
 |-  ( Fin i^i ( _V \ Fin ) ) = (/)
8 fun 
 |-  ( ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) : Fin --> NN0 /\ ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo } ) /\ ( Fin i^i ( _V \ Fin ) ) = (/) ) -> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) : ( Fin u. ( _V \ Fin ) ) --> ( NN0 u. { +oo } ) )
9 6 7 8 mp2an 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) : ( Fin u. ( _V \ Fin ) ) --> ( NN0 u. { +oo } )
10 df-hash 
 |-  # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )
11 eqid 
 |-  _V = _V
12 df-xnn0 
 |-  NN0* = ( NN0 u. { +oo } )
13 feq123 
 |-  ( ( # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) /\ _V = _V /\ NN0* = ( NN0 u. { +oo } ) ) -> ( # : _V --> NN0* <-> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) : _V --> ( NN0 u. { +oo } ) ) )
14 10 11 12 13 mp3an 
 |-  ( # : _V --> NN0* <-> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) : _V --> ( NN0 u. { +oo } ) )
15 unvdif 
 |-  ( Fin u. ( _V \ Fin ) ) = _V
16 15 feq2i 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) : ( Fin u. ( _V \ Fin ) ) --> ( NN0 u. { +oo } ) <-> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) : _V --> ( NN0 u. { +oo } ) )
17 14 16 bitr4i 
 |-  ( # : _V --> NN0* <-> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) : ( Fin u. ( _V \ Fin ) ) --> ( NN0 u. { +oo } ) )
18 9 17 mpbir 
 |-  # : _V --> NN0*