Theorem hashfxnn0

Description: The size function is a function into the extended nonnegative integers. (Contributed by Mario Carneiro, 13-Sep-2013) (Revised by AV, 10-Dec-2020)

	Ref	Expression
Assertion	hashfxnn0	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
2		eqid	$$⊢\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}=\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}$$
3	1 2	hashkf	$$⊢\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right):\mathrm{Fin}⟶{\mathbb{N}}_0$$
4		pnfex	$$⊢\mathrm{+\infty }\in \mathrm{V}$$
5	4	fconst	$$⊢\left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right):\mathrm{V}\setminus \mathrm{Fin}⟶\left\{\mathrm{+\infty }\right\}$$
6	3 5	pm3.2i	$$⊢\left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right):\mathrm{Fin}⟶{\mathbb{N}}_0\wedge \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right):\mathrm{V}\setminus \mathrm{Fin}⟶\left\{\mathrm{+\infty }\right\}\right)$$
7		disjdif	$$⊢\mathrm{Fin}\cap \left(\mathrm{V}\setminus \mathrm{Fin}\right)=\varnothing$$
8		fun	$$⊢\left(\left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right):\mathrm{Fin}⟶{\mathbb{N}}_0\wedge \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right):\mathrm{V}\setminus \mathrm{Fin}⟶\left\{\mathrm{+\infty }\right\}\right)\wedge \mathrm{Fin}\cap \left(\mathrm{V}\setminus \mathrm{Fin}\right)=\varnothing \right)\to \left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\right):\mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{Fin}\right)⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
9	6 7 8	mp2an	$$⊢\left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\right):\mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{Fin}\right)⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
10		df-hash	$$⊢\left|.\right|=\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)$$
11		eqid	$$⊢\mathrm{V}=\mathrm{V}$$
12		df-xnn0	$$⊢{\mathbb{N}}_0^{*}={\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
13		feq123	$$⊢\left(\left|.\right|=\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\wedge \mathrm{V}=\mathrm{V}\wedge {\mathbb{N}}_0^{*}={\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)\to \left(\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}\leftrightarrow \left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\right):\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)$$
14	10 11 12 13	mp3an	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}\leftrightarrow \left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\right):\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
15		unvdif	$$⊢\mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{Fin}\right)=\mathrm{V}$$
16	15	feq2i	$$⊢\left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\right):\mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{Fin}\right)⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\leftrightarrow \left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\right):\mathrm{V}⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
17	14 16	bitr4i	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}\leftrightarrow \left(\left(\left({\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}\right)\circ \mathrm{card}\right)\cup \left(\left(\mathrm{V}\setminus \mathrm{Fin}\right)\times \left\{\mathrm{+\infty }\right\}\right)\right):\mathrm{Fin}\cup \left(\mathrm{V}\setminus \mathrm{Fin}\right)⟶{\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}$$
18	9 17	mpbir	$$⊢\left|.\right|:\mathrm{V}⟶{\mathbb{N}}_0^{*}$$