Definition df-ackbij

Description: Define the Ackermann bijection from hereditarily finite sets to _om . This definition is derived from ackbij2 . (Contributed by Eric Schmidt, 24-Oct-2026)

	Ref	Expression
Assertion	df-ackbij	Could not format assertion : No typesetting found for |- ackBij = U. ( rec ( ( x e. _V |-> ( y e. ~P dom x |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) ) ) , (/) ) " _om ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cackbij	Could not format ackBij : No typesetting found for class ackBij with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5	4	cdm	$$class\mathrm{dom}x$$
6	5	cpw	$$class𝒫\mathrm{dom}x$$
7		vz	$$setvarz$$
8		com	$$class\mathrm{\omega }$$
9	8	cpw	$$class𝒫\mathrm{\omega }$$
10		cfn	$$class\mathrm{Fin}$$
11	9 10	cin	$$class\left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)$$
12		ccrd	$$class\mathrm{card}$$
13		vw	$$setvarw$$
14	7	cv	$$setvarz$$
15	13	cv	$$setvarw$$
16	15	csn	$$class\left\{w\right\}$$
17	15	cpw	$$class𝒫w$$
18	16 17	cxp	$$class\left(\left\{w\right\}\times 𝒫w\right)$$
19	13 14 18	ciun	$$class\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)$$
20	19 12	cfv	$$class\mathrm{card}\left(\bigcup _{w\in z}\left(\left\{w\right\}\times 𝒫w\right)\right)$$
21	7 11 20	cmpt	$$class\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)$$
22	3	cv	$$setvary$$
23	4 22	cima	$$classx\left[y\right]$$
24	23 21	cfv	$$class\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\left[y\right]\right)$$
25	3 6 24	cmpt	$$class\left(y\in 𝒫\mathrm{dom}x⟼\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\left[y\right]\right)\right)$$
26	1 2 25	cmpt	$$class\left(x\in \mathrm{V}⟼\left(y\in 𝒫\mathrm{dom}x⟼\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\left[y\right]\right)\right)\right)$$
27		c0	$$class\varnothing$$
28	26 27	crdg	$$class\mathrm{rec}\left(\left(x\in \mathrm{V}⟼\left(y\in 𝒫\mathrm{dom}x⟼\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\left[y\right]\right)\right)\right),\varnothing \right)$$
29	28 8	cima	$$class\mathrm{rec}\left(\left(x\in \mathrm{V}⟼\left(y\in 𝒫\mathrm{dom}x⟼\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\left[y\right]\right)\right)\right),\varnothing \right)\left[\mathrm{\omega }\right]$$
30	29	cuni	$$class\bigcup \mathrm{rec}\left(\left(x\in \mathrm{V}⟼\left(y\in 𝒫\mathrm{dom}x⟼\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\left[y\right]\right)\right)\right),\varnothing \right)\left[\mathrm{\omega }\right]$$
31	0 30	wceq	Could not format ackBij = U. ( rec ( ( x e. _V |-> ( y e. ~P dom x |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) ) ) , (/) ) " _om ) : No typesetting found for wff ackBij = U. ( rec ( ( x e. _V |-> ( y e. ~P dom x |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) ) ) , (/) ) " _om ) with typecode wff