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

Metamath Proof Explorer

Theorem hashf

Description: The size function maps all finite sets to their cardinality, as members of NN0 , and infinite sets to +oo . TODO-AV: mark as OBSOLETE and replace it by hashfxnn0 ? (Contributed by Mario Carneiro, 13-Sep-2013) (Revised by Mario Carneiro, 13-Jul-2014) (Proof shortened by AV, 24-Oct-2021)

Ref Expression
Assertion hashf 
|- # : _V --> ( NN0 u. { +oo } )

Proof

Step Hyp Ref Expression
1 hashfxnn0 
 |-  # : _V --> NN0*
2 eqid 
 |-  _V = _V
3 df-xnn0 
 |-  NN0* = ( NN0 u. { +oo } )
4 3 eqcomi 
 |-  ( NN0 u. { +oo } ) = NN0*
5 2 4 feq23i 
 |-  ( # : _V --> ( NN0 u. { +oo } ) <-> # : _V --> NN0* )
6 1 5 mpbir 
 |-  # : _V --> ( NN0 u. { +oo } )