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	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$

Proof

Step	Hyp	Ref	Expression
1		hashfxnn0	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}$$
2		eqid	$$⊢\mathrm{V}=\mathrm{V}$$
3		df-xnn0	$$⊢{\mathbb{N}}_0^{*}={\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
4	3	eqcomi	$$⊢{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}={\mathbb{N}}_0^{*}$$
5	2 4	feq23i	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\leftrightarrow \left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}$$
6	1 5	mpbir	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$