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