Theorem ackbijnn

Description: Translate the Ackermann bijection ackbij1 onto the positive integers. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypothesis	ackbijnn.1	$$⊢F=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\sum _{y\in x}{2}^y\right)$$
Assertion	ackbijnn	$$⊢F:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		ackbijnn.1	$$⊢F=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\sum _{y\in x}{2}^y\right)$$
2		hashgval2	$$⊢{\left|.\right|\upharpoonright }_{\mathrm{\omega }}={\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x+1\right),0\right)\upharpoonright }_{\mathrm{\omega }}$$
3	2	hashgf1o	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
4		sneq	$$⊢w=y\to \left\{w\right\}=\left\{y\right\}$$
5		pweq	$$⊢w=y\to 𝒫w=𝒫y$$
6	4 5	xpeq12d	$$⊢w=y\to \left\{w\right\}\times 𝒫w=\left\{y\right\}\times 𝒫y$$
7	6	cbviunv	$$⊢\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)=\bigcup _{y\in z}\left(\left\{y\right\}\times 𝒫y\right)$$
8		iuneq1	$$⊢z=x\to \bigcup _{y\in z}\left(\left\{y\right\}\times 𝒫y\right)=\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)$$
9	7 8	eqtrid	$$⊢z=x\to \bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)=\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)$$
10	9	fveq2d	$$⊢z=x\to \mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)=\mathrm{card}\left(\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)\right)$$
11	10	cbvmptv	$$⊢\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)=\left(x\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)\right)\right)$$
12	11	ackbij1	$$⊢\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right):𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}\mathrm{\omega }$$
13		f1ocnv	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathrm{\omega }$$
14	3 13	ax-mp	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathrm{\omega }$$
15		f1opwfi	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathrm{\omega }\to \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
16	14 15	ax-mp	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
17		f1oco	$$⊢\left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right):𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}\mathrm{\omega }\wedge \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\to \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}\mathrm{\omega }$$
18	12 16 17	mp2an	$$⊢\left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}\mathrm{\omega }$$
19		f1oco	$$⊢\left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\wedge \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}\mathrm{\omega }\right)\to \left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
20	3 18 19	mp2an	$$⊢\left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
21		inss2	$$⊢𝒫\mathrm{\omega }\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
22		f1of	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}𝒫\mathrm{\omega }\cap \mathrm{Fin}\to \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
23	16 22	ax-mp	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
24		eqid	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)$$
25	24	fmpt	$$⊢\forall x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right){\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\leftrightarrow \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}⟶𝒫\mathrm{\omega }\cap \mathrm{Fin}$$
26	23 25	mpbir	$$⊢\forall x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right){\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$
27	26	rspec	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$
28	21 27	sselid	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\in \mathrm{Fin}$$
29		snfi	$$⊢\left\{w\right\}\in \mathrm{Fin}$$
30		cnvimass	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\subseteq \mathrm{dom}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)$$
31		dmhashres	$$⊢\mathrm{dom}\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)=\mathrm{\omega }$$
32	30 31	sseqtri	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\subseteq \mathrm{\omega }$$
33		onfin2	$$⊢\mathrm{\omega }=\mathrm{On}\cap \mathrm{Fin}$$
34		inss2	$$⊢\mathrm{On}\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
35	33 34	eqsstri	$$⊢\mathrm{\omega }\subseteq \mathrm{Fin}$$
36	32 35	sstri	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\subseteq \mathrm{Fin}$$
37		simpr	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\to w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]$$
38	36 37	sselid	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\to w\in \mathrm{Fin}$$
39		pwfi	$$⊢w\in \mathrm{Fin}\leftrightarrow 𝒫w\in \mathrm{Fin}$$
40	38 39	sylib	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\to 𝒫w\in \mathrm{Fin}$$
41		xpfi	$$⊢\left(\left\{w\right\}\in \mathrm{Fin}\wedge 𝒫w\in \mathrm{Fin}\right)\to \left\{w\right\}\times 𝒫w\in \mathrm{Fin}$$
42	29 40 41	sylancr	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\to \left\{w\right\}\times 𝒫w\in \mathrm{Fin}$$
43	42	ralrimiva	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \forall w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\left\{w\right\}\times 𝒫w\in \mathrm{Fin}$$
44		iunfi	$$⊢\left({\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\in \mathrm{Fin}\wedge \forall w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\left\{w\right\}\times 𝒫w\in \mathrm{Fin}\right)\to \bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\in \mathrm{Fin}$$
45	28 43 44	syl2anc	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\in \mathrm{Fin}$$
46		ficardom	$$⊢\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\in \mathrm{Fin}\to \mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\in \mathrm{\omega }$$
47	45 46	syl	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\in \mathrm{\omega }$$
48	47	fvresd	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)=\left|\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right|$$
49		hashcard	$$⊢\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\in \mathrm{Fin}\to \left|\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right|=\left|\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right|$$
50	45 49	syl	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \left|\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right|=\left|\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right|$$
51		xp1st	$$⊢z\in \left(\left\{w\right\}\times 𝒫w\right)\to 1^{st}\left(z\right)\in \left\{w\right\}$$
52		elsni	$$⊢1^{st}\left(z\right)\in \left\{w\right\}\to 1^{st}\left(z\right)=w$$
53	51 52	syl	$$⊢z\in \left(\left\{w\right\}\times 𝒫w\right)\to 1^{st}\left(z\right)=w$$
54	53	rgen	$$⊢\forall z\in \left(\left\{w\right\}\times 𝒫w\right)1^{st}\left(z\right)=w$$
55	54	rgenw	$$⊢\forall w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\forall z\in \left(\left\{w\right\}\times 𝒫w\right)1^{st}\left(z\right)=w$$
56		invdisj	$$⊢\forall w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\forall z\in \left(\left\{w\right\}\times 𝒫w\right)1^{st}\left(z\right)=w\to \underset{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}{Disj}\left(\left\{w\right\}\times 𝒫w\right)$$
57	55 56	mp1i	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \underset{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}{Disj}\left(\left\{w\right\}\times 𝒫w\right)$$
58	28 42 57	hashiun	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \left|\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right|=\sum _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left|\left\{w\right\}\times 𝒫w\right|$$
59		sneq	$$⊢w={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\to \left\{w\right\}=\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}$$
60		pweq	$$⊢w={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\to 𝒫w=𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)$$
61	59 60	xpeq12d	$$⊢w={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\to \left\{w\right\}\times 𝒫w=\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\times 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)$$
62	61	fveq2d	$$⊢w={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\to \left|\left\{w\right\}\times 𝒫w\right|=\left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\times 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|$$
63		elinel2	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to x\in \mathrm{Fin}$$
64		f1of1	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathrm{\omega }\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathrm{\omega }$$
65	14 64	ax-mp	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathrm{\omega }$$
66		elinel1	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to x\in 𝒫{\mathbb{N}}_0$$
67	66	elpwid	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to x\subseteq {\mathbb{N}}_0$$
68		f1ores	$$⊢\left({\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1}{⟶}\mathrm{\omega }\wedge x\subseteq {\mathbb{N}}_0\right)\to \left({{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]$$
69	65 67 68	sylancr	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \left({{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\upharpoonright }_x\right):x\underset{1-1\; onto}{⟶}{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]$$
70		fvres	$$⊢y\in x\to \left({{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\upharpoonright }_x\right)\left(y\right)={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)$$
71	70	adantl	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left({{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\upharpoonright }_x\right)\left(y\right)={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)$$
72		hashcl	$$⊢\left\{w\right\}\times 𝒫w\in \mathrm{Fin}\to \left|\left\{w\right\}\times 𝒫w\right|\in {\mathbb{N}}_0$$
73		nn0cn	$$⊢\left|\left\{w\right\}\times 𝒫w\right|\in {\mathbb{N}}_0\to \left|\left\{w\right\}\times 𝒫w\right|\in ℂ$$
74	42 72 73	3syl	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\to \left|\left\{w\right\}\times 𝒫w\right|\in ℂ$$
75	62 63 69 71 74	fsumf1o	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \sum _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left|\left\{w\right\}\times 𝒫w\right|=\sum _{y\in x}\left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\times 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|$$
76		snfi	$$⊢\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\in \mathrm{Fin}$$
77	67	sselda	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to y\in {\mathbb{N}}_0$$
78		f1of	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathrm{\omega }\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0⟶\mathrm{\omega }$$
79	14 78	ax-mp	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}:{\mathbb{N}}_0⟶\mathrm{\omega }$$
80	79	ffvelcdmi	$$⊢y\in {\mathbb{N}}_0\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{\omega }$$
81	77 80	syl	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{\omega }$$
82	35 81	sselid	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{Fin}$$
83		pwfi	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{Fin}\leftrightarrow 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{Fin}$$
84	82 83	sylib	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{Fin}$$
85		hashxp	$$⊢\left(\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\in \mathrm{Fin}\wedge 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{Fin}\right)\to \left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\times 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=\left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\right|\left|𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|$$
86	76 84 85	sylancr	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\times 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=\left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\right|\left|𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|$$
87		hashsng	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{\omega }\to \left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\right|=1$$
88	81 87	syl	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\right|=1$$
89		hashpw	$$⊢{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\in \mathrm{Fin}\to \left|𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=2^{\left|{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|}$$
90	82 89	syl	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left|𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=2^{\left|{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|}$$
91	81	fvresd	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left({\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right)=\left|{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|$$
92		f1ocnvfv2	$$⊢\left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left({\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right)=y$$
93	3 77 92	sylancr	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left({\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right)=y$$
94	91 93	eqtr3d	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left|{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=y$$
95	94	oveq2d	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to 2^{\left|{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|}=2^y$$
96	90 95	eqtrd	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left|𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=2^y$$
97	88 96	oveq12d	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\right|\left|𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=12^y$$
98		2cn	$$⊢2\in ℂ$$
99		expcl	$$⊢\left(2\in ℂ\wedge y\in {\mathbb{N}}_0\right)\to 2^y\in ℂ$$
100	98 77 99	sylancr	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to 2^y\in ℂ$$
101	100	mullidd	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to 12^y=2^y$$
102	86 97 101	3eqtrd	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\wedge y\in x\right)\to \left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\times 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=2^y$$
103	102	sumeq2dv	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \sum _{y\in x}\left|\left\{{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right\}\times 𝒫{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left(y\right)\right|=\sum _{y\in x}{2}^y$$
104	58 75 103	3eqtrd	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \left|\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right|=\sum _{y\in x}{2}^y$$
105	48 50 104	3eqtrd	$$⊢x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)=\sum _{y\in x}{2}^y$$
106	105	mpteq2ia	$$⊢\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\right)=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\sum _{y\in x}{2}^y\right)$$
107	47	adantl	$$⊢\left(\top \wedge x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\right)\to \mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\in \mathrm{\omega }$$
108	27	adantl	$$⊢\left(\top \wedge x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)\right)\to {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$
109		eqidd	$$⊢\top \to \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)$$
110		eqidd	$$⊢\top \to \left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)=\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)$$
111		iuneq1	$$⊢z={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\to \bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)=\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)$$
112	111	fveq2d	$$⊢z={\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\to \mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)=\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)$$
113	108 109 110 112	fmptco	$$⊢\top \to \left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)$$
114		f1of	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }⟶{\mathbb{N}}_0$$
115	3 114	mp1i	$$⊢\top \to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right):\mathrm{\omega }⟶{\mathbb{N}}_0$$
116	115	feqmptd	$$⊢\top \to {\left|.\right|\upharpoonright }_{\mathrm{\omega }}=\left(y\in \mathrm{\omega }⟼\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(y\right)\right)$$
117		fveq2	$$⊢y=\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(y\right)=\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)$$
118	107 113 116 117	fmptco	$$⊢\top \to \left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\right)$$
119	118	mptru	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)=\left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\left(\mathrm{card}\left(\bigcup _{w\in {\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\right)$$
120	106 119 1	3eqtr4i	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)=F$$
121		f1oeq1	$$⊢\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)=F\to \left(\left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\leftrightarrow F:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\right)$$
122	120 121	ax-mp	$$⊢\left(\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)\circ \left(\left(z\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)\right)\circ \left(x\in \left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)⟼{\left({\left|.\right|\upharpoonright }_{\mathrm{\omega }}\right)}^{-1}\left[x\right]\right)\right)\right):𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\leftrightarrow F:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
123	20 122	mpbi	$$⊢F:𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$