Theorem hashomf1o

Description: The # function yields a bijection from _om to NN0 . (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashomf1o	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		hashgval2	$$⊢{\left|.\right|\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
2	1	hashgf1o	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$