Metamath Proof Explorer

Theorem ackbij3

Description: The Ackermann bijection is a bijection. This is just a restatement of ackbij2 . (Contributed by Eric Schmidt, 24-Oct-2026)

Ref Expression
Assertion ackbij3 
|- ackBij : HF -1-1-onto-> _om

Proof

Step Hyp Ref Expression
1 iuneq1 
 |-  ( z = u -> U_ w e. z ( { w } X. ~P w ) = U_ w e. u ( { w } X. ~P w ) )
2 1 fveq2d 
 |-  ( z = u -> ( card ` U_ w e. z ( { w } X. ~P w ) ) = ( card ` U_ w e. u ( { w } X. ~P w ) ) )
3 2 cbvmptv 
 |-  ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) = ( u e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. u ( { w } X. ~P w ) ) )
4 sneq 
 |-  ( w = v -> { w } = { v } )
5 pweq 
 |-  ( w = v -> ~P w = ~P v )
6 4 5 xpeq12d 
 |-  ( w = v -> ( { w } X. ~P w ) = ( { v } X. ~P v ) )
7 6 cbviunv 
 |-  U_ w e. u ( { w } X. ~P w ) = U_ v e. u ( { v } X. ~P v )
8 7 fveq2i 
 |-  ( card ` U_ w e. u ( { w } X. ~P w ) ) = ( card ` U_ v e. u ( { v } X. ~P v ) )
9 8 mpteq2i 
 |-  ( u e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. u ( { w } X. ~P w ) ) ) = ( u e. ( ~P _om i^i Fin ) |-> ( card ` U_ v e. u ( { v } X. ~P v ) ) )
10 3 9 eqtri 
 |-  ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) = ( u e. ( ~P _om i^i Fin ) |-> ( card ` U_ v e. u ( { v } X. ~P v ) ) )
11 dmeq 
 |-  ( x = u -> dom x = dom u )
12 11 pweqd 
 |-  ( x = u -> ~P dom x = ~P dom u )
13 imaeq1 
 |-  ( x = u -> ( x " y ) = ( u " y ) )
14 13 fveq2d 
 |-  ( x = u -> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) = ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " y ) ) )
15 12 14 mpteq12dv 
 |-  ( x = u -> ( y e. ~P dom x |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( x " y ) ) ) = ( y e. ~P dom u |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " y ) ) ) )
16 15 cbvmptv 
 |-  ( 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 ) ) ) ) = ( u e. _V |-> ( y e. ~P dom u |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " y ) ) ) )
17 imaeq2 
 |-  ( y = v -> ( u " y ) = ( u " v ) )
18 17 fveq2d 
 |-  ( y = v -> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " y ) ) = ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " v ) ) )
19 18 cbvmptv 
 |-  ( y e. ~P dom u |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " y ) ) ) = ( v e. ~P dom u |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " v ) ) )
20 19 mpteq2i 
 |-  ( u e. _V |-> ( y e. ~P dom u |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " y ) ) ) ) = ( u e. _V |-> ( v e. ~P dom u |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " v ) ) ) )
21 16 20 eqtri 
 |-  ( 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 ) ) ) ) = ( u e. _V |-> ( v e. ~P dom u |-> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) ` ( u " v ) ) ) )
22 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 )
23 10 21 22 ackbij2 
 |-  ackBij : HF -1-1-onto-> _om