Metamath Proof Explorer

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 = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ y e. x ( 2 ^ y ) )
Assertion ackbijnn 
|- F : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0

Proof

Step Hyp Ref Expression
1 ackbijnn.1 
 |-  F = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ y e. x ( 2 ^ y ) )
2 hashgval2 
 |-  ( # |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
3 2 hashgf1o 
 |-  ( # |` _om ) : _om -1-1-onto-> NN0
4 sneq 
 |-  ( w = y -> { w } = { y } )
5 pweq 
 |-  ( w = y -> ~P w = ~P y )
6 4 5 xpeq12d 
 |-  ( w = y -> ( { w } X. ~P w ) = ( { y } X. ~P y ) )
7 6 cbviunv 
 |-  U_ w e. z ( { w } X. ~P w ) = U_ y e. z ( { y } X. ~P y )
8 iuneq1 
 |-  ( z = x -> U_ y e. z ( { y } X. ~P y ) = U_ y e. x ( { y } X. ~P y ) )
9 7 8 syl5eq 
 |-  ( z = x -> U_ w e. z ( { w } X. ~P w ) = U_ y e. x ( { y } X. ~P y ) )
10 9 fveq2d 
 |-  ( z = x -> ( card ` U_ w e. z ( { w } X. ~P w ) ) = ( card ` U_ y e. x ( { y } X. ~P y ) ) )
11 10 cbvmptv 
 |-  ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) = ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ y e. x ( { y } X. ~P y ) ) )
12 11 ackbij1 
 |-  ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) : ( ~P _om i^i Fin ) -1-1-onto-> _om
13 f1ocnv 
 |-  ( ( # |` _om ) : _om -1-1-onto-> NN0 -> `' ( # |` _om ) : NN0 -1-1-onto-> _om )
14 3 13 ax-mp 
 |-  `' ( # |` _om ) : NN0 -1-1-onto-> _om
15 f1opwfi 
 |-  ( `' ( # |` _om ) : NN0 -1-1-onto-> _om -> ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> ( ~P _om i^i Fin ) )
16 14 15 ax-mp 
 |-  ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> ( ~P _om i^i Fin )
17 f1oco 
 |-  ( ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) : ( ~P _om i^i Fin ) -1-1-onto-> _om /\ ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> ( ~P _om i^i Fin ) ) -> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> _om )
18 12 16 17 mp2an 
 |-  ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> _om
19 f1oco 
 |-  ( ( ( # |` _om ) : _om -1-1-onto-> NN0 /\ ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> _om ) -> ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
20 3 18 19 mp2an 
 |-  ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0
21 inss2 
 |-  ( ~P _om i^i Fin ) C_ Fin
22 f1of 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> ( ~P _om i^i Fin ) -> ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) : ( ~P NN0 i^i Fin ) --> ( ~P _om i^i Fin ) )
23 16 22 ax-mp 
 |-  ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) : ( ~P NN0 i^i Fin ) --> ( ~P _om i^i Fin )
24 eqid 
 |-  ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) )
25 24 fmpt 
 |-  ( A. x e. ( ~P NN0 i^i Fin ) ( `' ( # |` _om ) " x ) e. ( ~P _om i^i Fin ) <-> ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) : ( ~P NN0 i^i Fin ) --> ( ~P _om i^i Fin ) )
26 23 25 mpbir 
 |-  A. x e. ( ~P NN0 i^i Fin ) ( `' ( # |` _om ) " x ) e. ( ~P _om i^i Fin )
27 26 rspec 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( `' ( # |` _om ) " x ) e. ( ~P _om i^i Fin ) )
28 21 27 sseldi 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( `' ( # |` _om ) " x ) e. Fin )
29 snfi 
 |-  { w } e. Fin
30 cnvimass 
 |-  ( `' ( # |` _om ) " x ) C_ dom ( # |` _om )
31 dmhashres 
 |-  dom ( # |` _om ) = _om
32 30 31 sseqtri 
 |-  ( `' ( # |` _om ) " x ) C_ _om
33 onfin2 
 |-  _om = ( On i^i Fin )
34 inss2 
 |-  ( On i^i Fin ) C_ Fin
35 33 34 eqsstri 
 |-  _om C_ Fin
36 32 35 sstri 
 |-  ( `' ( # |` _om ) " x ) C_ Fin
37 simpr 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ w e. ( `' ( # |` _om ) " x ) ) -> w e. ( `' ( # |` _om ) " x ) )
38 36 37 sseldi 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ w e. ( `' ( # |` _om ) " x ) ) -> w e. Fin )
39 pwfi 
 |-  ( w e. Fin <-> ~P w e. Fin )
40 38 39 sylib 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ w e. ( `' ( # |` _om ) " x ) ) -> ~P w e. Fin )
41 xpfi 
 |-  ( ( { w } e. Fin /\ ~P w e. Fin ) -> ( { w } X. ~P w ) e. Fin )
42 29 40 41 sylancr 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ w e. ( `' ( # |` _om ) " x ) ) -> ( { w } X. ~P w ) e. Fin )
43 42 ralrimiva 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> A. w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) e. Fin )
44 iunfi 
 |-  ( ( ( `' ( # |` _om ) " x ) e. Fin /\ A. w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) e. Fin ) -> U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) e. Fin )
45 28 43 44 syl2anc 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) e. Fin )
46 ficardom 
 |-  ( U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) e. Fin -> ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) e. _om )
47 45 46 syl 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) e. _om )
48 47 fvresd 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( ( # |` _om ) ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) = ( # ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) )
49 hashcard 
 |-  ( U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) e. Fin -> ( # ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) = ( # ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) )
50 45 49 syl 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( # ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) = ( # ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) )
51 xp1st 
 |-  ( z e. ( { w } X. ~P w ) -> ( 1st ` z ) e. { w } )
52 elsni 
 |-  ( ( 1st ` z ) e. { w } -> ( 1st ` z ) = w )
53 51 52 syl 
 |-  ( z e. ( { w } X. ~P w ) -> ( 1st ` z ) = w )
54 53 rgen 
 |-  A. z e. ( { w } X. ~P w ) ( 1st ` z ) = w
55 54 rgenw 
 |-  A. w e. ( `' ( # |` _om ) " x ) A. z e. ( { w } X. ~P w ) ( 1st ` z ) = w
56 invdisj 
 |-  ( A. w e. ( `' ( # |` _om ) " x ) A. z e. ( { w } X. ~P w ) ( 1st ` z ) = w -> Disj_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) )
57 55 56 mp1i 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> Disj_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) )
58 28 42 57 hashiun 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( # ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) = sum_ w e. ( `' ( # |` _om ) " x ) ( # ` ( { w } X. ~P w ) ) )
59 sneq 
 |-  ( w = ( `' ( # |` _om ) ` y ) -> { w } = { ( `' ( # |` _om ) ` y ) } )
60 pweq 
 |-  ( w = ( `' ( # |` _om ) ` y ) -> ~P w = ~P ( `' ( # |` _om ) ` y ) )
61 59 60 xpeq12d 
 |-  ( w = ( `' ( # |` _om ) ` y ) -> ( { w } X. ~P w ) = ( { ( `' ( # |` _om ) ` y ) } X. ~P ( `' ( # |` _om ) ` y ) ) )
62 61 fveq2d 
 |-  ( w = ( `' ( # |` _om ) ` y ) -> ( # ` ( { w } X. ~P w ) ) = ( # ` ( { ( `' ( # |` _om ) ` y ) } X. ~P ( `' ( # |` _om ) ` y ) ) ) )
63 elinel2 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> x e. Fin )
64 f1of1 
 |-  ( `' ( # |` _om ) : NN0 -1-1-onto-> _om -> `' ( # |` _om ) : NN0 -1-1-> _om )
65 14 64 ax-mp 
 |-  `' ( # |` _om ) : NN0 -1-1-> _om
66 elinel1 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> x e. ~P NN0 )
67 66 elpwid 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> x C_ NN0 )
68 f1ores 
 |-  ( ( `' ( # |` _om ) : NN0 -1-1-> _om /\ x C_ NN0 ) -> ( `' ( # |` _om ) |` x ) : x -1-1-onto-> ( `' ( # |` _om ) " x ) )
69 65 67 68 sylancr 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( `' ( # |` _om ) |` x ) : x -1-1-onto-> ( `' ( # |` _om ) " x ) )
70 fvres 
 |-  ( y e. x -> ( ( `' ( # |` _om ) |` x ) ` y ) = ( `' ( # |` _om ) ` y ) )
71 70 adantl 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( ( `' ( # |` _om ) |` x ) ` y ) = ( `' ( # |` _om ) ` y ) )
72 hashcl 
 |-  ( ( { w } X. ~P w ) e. Fin -> ( # ` ( { w } X. ~P w ) ) e. NN0 )
73 nn0cn 
 |-  ( ( # ` ( { w } X. ~P w ) ) e. NN0 -> ( # ` ( { w } X. ~P w ) ) e. CC )
74 42 72 73 3syl 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ w e. ( `' ( # |` _om ) " x ) ) -> ( # ` ( { w } X. ~P w ) ) e. CC )
75 62 63 69 71 74 fsumf1o 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> sum_ w e. ( `' ( # |` _om ) " x ) ( # ` ( { w } X. ~P w ) ) = sum_ y e. x ( # ` ( { ( `' ( # |` _om ) ` y ) } X. ~P ( `' ( # |` _om ) ` y ) ) ) )
76 snfi 
 |-  { ( `' ( # |` _om ) ` y ) } e. Fin
77 67 sselda 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> y e. NN0 )
78 f1of 
 |-  ( `' ( # |` _om ) : NN0 -1-1-onto-> _om -> `' ( # |` _om ) : NN0 --> _om )
79 14 78 ax-mp 
 |-  `' ( # |` _om ) : NN0 --> _om
80 79 ffvelrni 
 |-  ( y e. NN0 -> ( `' ( # |` _om ) ` y ) e. _om )
81 77 80 syl 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( `' ( # |` _om ) ` y ) e. _om )
82 35 81 sseldi 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( `' ( # |` _om ) ` y ) e. Fin )
83 pwfi 
 |-  ( ( `' ( # |` _om ) ` y ) e. Fin <-> ~P ( `' ( # |` _om ) ` y ) e. Fin )
84 82 83 sylib 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ~P ( `' ( # |` _om ) ` y ) e. Fin )
85 hashxp 
 |-  ( ( { ( `' ( # |` _om ) ` y ) } e. Fin /\ ~P ( `' ( # |` _om ) ` y ) e. Fin ) -> ( # ` ( { ( `' ( # |` _om ) ` y ) } X. ~P ( `' ( # |` _om ) ` y ) ) ) = ( ( # ` { ( `' ( # |` _om ) ` y ) } ) x. ( # ` ~P ( `' ( # |` _om ) ` y ) ) ) )
86 76 84 85 sylancr 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( # ` ( { ( `' ( # |` _om ) ` y ) } X. ~P ( `' ( # |` _om ) ` y ) ) ) = ( ( # ` { ( `' ( # |` _om ) ` y ) } ) x. ( # ` ~P ( `' ( # |` _om ) ` y ) ) ) )
87 hashsng 
 |-  ( ( `' ( # |` _om ) ` y ) e. _om -> ( # ` { ( `' ( # |` _om ) ` y ) } ) = 1 )
88 81 87 syl 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( # ` { ( `' ( # |` _om ) ` y ) } ) = 1 )
89 hashpw 
 |-  ( ( `' ( # |` _om ) ` y ) e. Fin -> ( # ` ~P ( `' ( # |` _om ) ` y ) ) = ( 2 ^ ( # ` ( `' ( # |` _om ) ` y ) ) ) )
90 82 89 syl 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( # ` ~P ( `' ( # |` _om ) ` y ) ) = ( 2 ^ ( # ` ( `' ( # |` _om ) ` y ) ) ) )
91 81 fvresd 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( ( # |` _om ) ` ( `' ( # |` _om ) ` y ) ) = ( # ` ( `' ( # |` _om ) ` y ) ) )
92 f1ocnvfv2 
 |-  ( ( ( # |` _om ) : _om -1-1-onto-> NN0 /\ y e. NN0 ) -> ( ( # |` _om ) ` ( `' ( # |` _om ) ` y ) ) = y )
93 3 77 92 sylancr 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( ( # |` _om ) ` ( `' ( # |` _om ) ` y ) ) = y )
94 91 93 eqtr3d 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( # ` ( `' ( # |` _om ) ` y ) ) = y )
95 94 oveq2d 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( 2 ^ ( # ` ( `' ( # |` _om ) ` y ) ) ) = ( 2 ^ y ) )
96 90 95 eqtrd 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( # ` ~P ( `' ( # |` _om ) ` y ) ) = ( 2 ^ y ) )
97 88 96 oveq12d 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( ( # ` { ( `' ( # |` _om ) ` y ) } ) x. ( # ` ~P ( `' ( # |` _om ) ` y ) ) ) = ( 1 x. ( 2 ^ y ) ) )
98 2cn 
 |-  2 e. CC
99 expcl 
 |-  ( ( 2 e. CC /\ y e. NN0 ) -> ( 2 ^ y ) e. CC )
100 98 77 99 sylancr 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( 2 ^ y ) e. CC )
101 100 mulid2d 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( 1 x. ( 2 ^ y ) ) = ( 2 ^ y ) )
102 86 97 101 3eqtrd 
 |-  ( ( x e. ( ~P NN0 i^i Fin ) /\ y e. x ) -> ( # ` ( { ( `' ( # |` _om ) ` y ) } X. ~P ( `' ( # |` _om ) ` y ) ) ) = ( 2 ^ y ) )
103 102 sumeq2dv 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> sum_ y e. x ( # ` ( { ( `' ( # |` _om ) ` y ) } X. ~P ( `' ( # |` _om ) ` y ) ) ) = sum_ y e. x ( 2 ^ y ) )
104 58 75 103 3eqtrd 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( # ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) = sum_ y e. x ( 2 ^ y ) )
105 48 50 104 3eqtrd 
 |-  ( x e. ( ~P NN0 i^i Fin ) -> ( ( # |` _om ) ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) = sum_ y e. x ( 2 ^ y ) )
106 105 mpteq2ia 
 |-  ( x e. ( ~P NN0 i^i Fin ) |-> ( ( # |` _om ) ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> sum_ y e. x ( 2 ^ y ) )
107 47 adantl 
 |-  ( ( T. /\ x e. ( ~P NN0 i^i Fin ) ) -> ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) e. _om )
108 27 adantl 
 |-  ( ( T. /\ x e. ( ~P NN0 i^i Fin ) ) -> ( `' ( # |` _om ) " x ) e. ( ~P _om i^i Fin ) )
109 eqidd 
 |-  ( T. -> ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) )
110 eqidd 
 |-  ( T. -> ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) = ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) )
111 iuneq1 
 |-  ( z = ( `' ( # |` _om ) " x ) -> U_ w e. z ( { w } X. ~P w ) = U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) )
112 111 fveq2d 
 |-  ( z = ( `' ( # |` _om ) " x ) -> ( card ` U_ w e. z ( { w } X. ~P w ) ) = ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) )
113 108 109 110 112 fmptco 
 |-  ( T. -> ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) )
114 f1of 
 |-  ( ( # |` _om ) : _om -1-1-onto-> NN0 -> ( # |` _om ) : _om --> NN0 )
115 3 114 mp1i 
 |-  ( T. -> ( # |` _om ) : _om --> NN0 )
116 115 feqmptd 
 |-  ( T. -> ( # |` _om ) = ( y e. _om |-> ( ( # |` _om ) ` y ) ) )
117 fveq2 
 |-  ( y = ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) -> ( ( # |` _om ) ` y ) = ( ( # |` _om ) ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) )
118 107 113 116 117 fmptco 
 |-  ( T. -> ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> ( ( # |` _om ) ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) ) )
119 118 mptru 
 |-  ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) = ( x e. ( ~P NN0 i^i Fin ) |-> ( ( # |` _om ) ` ( card ` U_ w e. ( `' ( # |` _om ) " x ) ( { w } X. ~P w ) ) ) )
120 106 119 1 3eqtr4i 
 |-  ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) = F
121 f1oeq1 
 |-  ( ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) = F -> ( ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 <-> F : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 ) )
122 120 121 ax-mp 
 |-  ( ( ( # |` _om ) o. ( ( z e. ( ~P _om i^i Fin ) |-> ( card ` U_ w e. z ( { w } X. ~P w ) ) ) o. ( x e. ( ~P NN0 i^i Fin ) |-> ( `' ( # |` _om ) " x ) ) ) ) : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 <-> F : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0 )
123 20 122 mpbi 
 |-  F : ( ~P NN0 i^i Fin ) -1-1-onto-> NN0