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

Proof

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