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 ⟶ ( ℕ0 ∪ { +∞ } )

Proof

Step	Hyp	Ref	Expression
1		hashfxnn0	⊢ ♯ : V ⟶ ℕ0*
2		eqid	⊢ V = V
3		df-xnn0	⊢ ℕ0* = ( ℕ0 ∪ { +∞ } )
4	3	eqcomi	⊢ ( ℕ0 ∪ { +∞ } ) = ℕ0*
5	2 4	feq23i	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) ↔ ♯ : V ⟶ ℕ0* )
6	1 5	mpbir	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )