Metamath Proof Explorer

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 
|- 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 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cackbij 
 |-  ackBij
1 vx 
 |-  x
2 cvv 
 |-  _V
3 vy 
 |-  y
4 1 cv 
 |-  x
5 4 cdm 
 |-  dom x
6 5 cpw 
 |-  ~P dom x
7 vz 
 |-  z
8 com 
 |-  _om
9 8 cpw 
 |-  ~P _om
10 cfn 
 |-  Fin
11 9 10 cin 
 |-  ( ~P _om i^i Fin )
12 ccrd 
 |-  card
13 vw 
 |-  w
14 7 cv 
 |-  z
15 13 cv 
 |-  w
16 15 csn 
 |-  { w }
17 15 cpw 
 |-  ~P w
18 16 17 cxp 
 |-  ( { w } X. ~P w )
19 13 14 18 ciun 
 |-  U_ w e. z ( { w } X. ~P w )
20 19 12 cfv 
 |-  ( card ` U_ w e. z ( { w } X. ~P w ) )
21 7 11 20 cmpt 
 |-  ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) )
22 3 cv 
 |-  y
23 4 22 cima 
 |-  ( x " y )
24 23 21 cfv 
 |-  ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) )
25 3 6 24 cmpt 
 |-  ( y e. ~P dom x |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) )
26 1 2 25 cmpt 
 |-  ( 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 ) ) ) )
27 c0 
 |-  (/)
28 26 27 crdg 
 |-  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 ) ) ) ) , (/) )
29 28 8 cima 
 |-  ( 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 )
30 29 cuni 
 |-  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 )
31 0 30 wceq 
 |-  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 )