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 ⟶ ℕ_{0} \cup \{+∞\}$

Proof

Step	Hyp	Ref	Expression
1		hashfxnn0	$⊢ \|.\| : V ⟶ ℕ_{0}^{*}$
2		eqid	$⊢ V = V$
3		df-xnn0	$⊢ ℕ_{0}^{*} = ℕ_{0} \cup \{+∞\}$
4	3	eqcomi	$⊢ ℕ_{0} \cup \{+∞\} = ℕ_{0}^{*}$
5	2 4	feq23i	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\} \leftrightarrow \|.\| : V ⟶ ℕ_{0}^{*}$
6	1 5	mpbir	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$