Theorem hashomiso

Description: The # function yields an order isomorphism between _om and NN0 . (Contributed by Eric Schmidt, 7-Jul-2026)

	Ref	Expression
Assertion	hashomiso	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right){Isom}_{\mathrm{E},<}\left(\mathrm{\omega },{\mathbb{N}}_0\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashomf1o	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
2		epel	$$⊢x\mathrm{E}y\leftrightarrow x\in y$$
3		hashnnltb	$$⊢\left(x\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \left(x\in y\leftrightarrow \left|x\right|<\left|y\right|\right)$$
4	2 3	bitrid	$$⊢\left(x\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \left(x\mathrm{E}y\leftrightarrow \left|x\right|<\left|y\right|\right)$$
5		fvres	$$⊢x\in \mathrm{\omega }\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(x\right)=\left|x\right|$$
6		fvres	$$⊢y\in \mathrm{\omega }\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(y\right)=\left|y\right|$$
7	5 6	breqan12d	$$⊢\left(x\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(x\right)<\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(y\right)\leftrightarrow \left|x\right|<\left|y\right|\right)$$
8	4 7	bitr4d	$$⊢\left(x\in \mathrm{\omega }\wedge y\in \mathrm{\omega }\right)\to \left(x\mathrm{E}y\leftrightarrow \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(x\right)<\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(y\right)\right)$$
9	8	rgen2	$$⊢\forall x\in \mathrm{\omega }\forall y\in \mathrm{\omega }\left(x\mathrm{E}y\leftrightarrow \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(x\right)<\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(y\right)\right)$$
10		df-isom	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right){Isom}_{\mathrm{E},<}\left(\mathrm{\omega },{\mathbb{N}}_0\right)\leftrightarrow \left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\wedge \forall x\in \mathrm{\omega }\forall y\in \mathrm{\omega }\left(x\mathrm{E}y\leftrightarrow \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(x\right)<\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(y\right)\right)\right)$$
11	1 9 10	mpbir2an	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right){Isom}_{\mathrm{E},<}\left(\mathrm{\omega },{\mathbb{N}}_0\right)$$