Metamath Proof Explorer

Theorem eulerpartlemgh

Description: Lemma for eulerpart : The F function is a bijection on the U subsets. (Contributed by Thierry Arnoux, 15-Aug-2018)

Ref Expression
Hypotheses eulerpart.p 
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
eulerpart.o 
|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
eulerpart.d 
|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
eulerpart.j 
|- J = { z e. NN | -. 2 || z }
eulerpart.f 
|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
eulerpart.h 
|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
eulerpart.m 
|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
eulerpart.r 
|- R = { f | ( `' f " NN ) e. Fin }
eulerpart.t 
|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
eulerpart.g 
|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
eulerpartlemgh.1 
|- U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) )
Assertion eulerpartlemgh 
|- ( A e. ( T i^i R ) -> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } )

Proof

Step Hyp Ref Expression
1 eulerpart.p 
 |-  P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2 eulerpart.o 
 |-  O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3 eulerpart.d 
 |-  D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4 eulerpart.j 
 |-  J = { z e. NN | -. 2 || z }
5 eulerpart.f 
 |-  F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6 eulerpart.h 
 |-  H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7 eulerpart.m 
 |-  M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8 eulerpart.r 
 |-  R = { f | ( `' f " NN ) e. Fin }
9 eulerpart.t 
 |-  T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
10 eulerpart.g 
 |-  G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
11 eulerpartlemgh.1 
 |-  U = U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) )
12 4 5 oddpwdc 
 |-  F : ( J X. NN0 ) -1-1-onto-> NN
13 f1of1 
 |-  ( F : ( J X. NN0 ) -1-1-onto-> NN -> F : ( J X. NN0 ) -1-1-> NN )
14 12 13 ax-mp 
 |-  F : ( J X. NN0 ) -1-1-> NN
15 iunss 
 |-  ( U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) <-> A. t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
16 inss2 
 |-  ( ( `' A " NN ) i^i J ) C_ J
17 16 sseli 
 |-  ( t e. ( ( `' A " NN ) i^i J ) -> t e. J )
18 17 snssd 
 |-  ( t e. ( ( `' A " NN ) i^i J ) -> { t } C_ J )
19 bitsss 
 |-  ( bits ` ( A ` t ) ) C_ NN0
20 xpss12 
 |-  ( ( { t } C_ J /\ ( bits ` ( A ` t ) ) C_ NN0 ) -> ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
21 18 19 20 sylancl 
 |-  ( t e. ( ( `' A " NN ) i^i J ) -> ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
22 15 21 mprgbir 
 |-  U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 )
23 11 22 eqsstri 
 |-  U C_ ( J X. NN0 )
24 f1ores 
 |-  ( ( F : ( J X. NN0 ) -1-1-> NN /\ U C_ ( J X. NN0 ) ) -> ( F |` U ) : U -1-1-onto-> ( F " U ) )
25 14 23 24 mp2an 
 |-  ( F |` U ) : U -1-1-onto-> ( F " U )
26 simpr 
 |-  ( ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) /\ ( ( 2 ^ n ) x. t ) = p ) -> ( ( 2 ^ n ) x. t ) = p )
27 2nn 
 |-  2 e. NN
28 27 a1i 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) -> 2 e. NN )
29 19 sseli 
 |-  ( n e. ( bits ` ( A ` t ) ) -> n e. NN0 )
30 29 adantl 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) -> n e. NN0 )
31 28 30 nnexpcld 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) -> ( 2 ^ n ) e. NN )
32 simplr 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) -> t e. NN )
33 31 32 nnmulcld 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) -> ( ( 2 ^ n ) x. t ) e. NN )
34 33 adantr 
 |-  ( ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) /\ ( ( 2 ^ n ) x. t ) = p ) -> ( ( 2 ^ n ) x. t ) e. NN )
35 26 34 eqeltrrd 
 |-  ( ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ n e. ( bits ` ( A ` t ) ) ) /\ ( ( 2 ^ n ) x. t ) = p ) -> p e. NN )
36 35 rexlimdva2 
 |-  ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> p e. NN ) )
37 36 rexlimdva 
 |-  ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> p e. NN ) )
38 37 pm4.71rd 
 |-  ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> ( p e. NN /\ E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) )
39 rex0 
 |-  -. E. n e. (/) ( ( 2 ^ n ) x. t ) = p
40 simplr 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> t e. NN )
41 simpr 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. t e. ( `' A " NN ) )
42 1 2 3 4 5 6 7 8 9 eulerpartlemt0 
 |-  ( A e. ( T i^i R ) <-> ( A e. ( NN0 ^m NN ) /\ ( `' A " NN ) e. Fin /\ ( `' A " NN ) C_ J ) )
43 42 simp1bi 
 |-  ( A e. ( T i^i R ) -> A e. ( NN0 ^m NN ) )
44 elmapi 
 |-  ( A e. ( NN0 ^m NN ) -> A : NN --> NN0 )
45 43 44 syl 
 |-  ( A e. ( T i^i R ) -> A : NN --> NN0 )
46 45 ad2antrr 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> A : NN --> NN0 )
47 ffn 
 |-  ( A : NN --> NN0 -> A Fn NN )
48 elpreima 
 |-  ( A Fn NN -> ( t e. ( `' A " NN ) <-> ( t e. NN /\ ( A ` t ) e. NN ) ) )
49 46 47 48 3syl 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( t e. ( `' A " NN ) <-> ( t e. NN /\ ( A ` t ) e. NN ) ) )
50 41 49 mtbid 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. ( t e. NN /\ ( A ` t ) e. NN ) )
51 imnan 
 |-  ( ( t e. NN -> -. ( A ` t ) e. NN ) <-> -. ( t e. NN /\ ( A ` t ) e. NN ) )
52 50 51 sylibr 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( t e. NN -> -. ( A ` t ) e. NN ) )
53 40 52 mpd 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. ( A ` t ) e. NN )
54 46 40 ffvelrnd 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( A ` t ) e. NN0 )
55 elnn0 
 |-  ( ( A ` t ) e. NN0 <-> ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) )
56 54 55 sylib 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) )
57 orel1 
 |-  ( -. ( A ` t ) e. NN -> ( ( ( A ` t ) e. NN \/ ( A ` t ) = 0 ) -> ( A ` t ) = 0 ) )
58 53 56 57 sylc 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( A ` t ) = 0 )
59 58 fveq2d 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( bits ` ( A ` t ) ) = ( bits ` 0 ) )
60 0bits 
 |-  ( bits ` 0 ) = (/)
61 59 60 eqtrdi 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( bits ` ( A ` t ) ) = (/) )
62 61 rexeqdv 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> ( E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> E. n e. (/) ( ( 2 ^ n ) x. t ) = p ) )
63 39 62 mtbiri 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. ( `' A " NN ) ) -> -. E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
64 63 ex 
 |-  ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( -. t e. ( `' A " NN ) -> -. E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
65 64 con4d 
 |-  ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> t e. ( `' A " NN ) ) )
66 65 impr 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> t e. ( `' A " NN ) )
67 eldif 
 |-  ( t e. ( NN \ J ) <-> ( t e. NN /\ -. t e. J ) )
68 1 2 3 4 5 6 7 8 9 eulerpartlemf 
 |-  ( ( A e. ( T i^i R ) /\ t e. ( NN \ J ) ) -> ( A ` t ) = 0 )
69 67 68 sylan2br 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. NN /\ -. t e. J ) ) -> ( A ` t ) = 0 )
70 69 anassrs 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> ( A ` t ) = 0 )
71 70 fveq2d 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> ( bits ` ( A ` t ) ) = ( bits ` 0 ) )
72 71 60 eqtrdi 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> ( bits ` ( A ` t ) ) = (/) )
73 72 rexeqdv 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> ( E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> E. n e. (/) ( ( 2 ^ n ) x. t ) = p ) )
74 39 73 mtbiri 
 |-  ( ( ( A e. ( T i^i R ) /\ t e. NN ) /\ -. t e. J ) -> -. E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
75 74 ex 
 |-  ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( -. t e. J -> -. E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
76 75 con4d 
 |-  ( ( A e. ( T i^i R ) /\ t e. NN ) -> ( E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> t e. J ) )
77 76 impr 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> t e. J )
78 66 77 elind 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> t e. ( ( `' A " NN ) i^i J ) )
79 simprr 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
80 78 79 jca 
 |-  ( ( A e. ( T i^i R ) /\ ( t e. NN /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) -> ( t e. ( ( `' A " NN ) i^i J ) /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
81 80 ex 
 |-  ( A e. ( T i^i R ) -> ( ( t e. NN /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) -> ( t e. ( ( `' A " NN ) i^i J ) /\ E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) )
82 81 reximdv2 
 |-  ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
83 ssrab2 
 |-  { z e. NN | -. 2 || z } C_ NN
84 4 83 eqsstri 
 |-  J C_ NN
85 16 84 sstri 
 |-  ( ( `' A " NN ) i^i J ) C_ NN
86 ssrexv 
 |-  ( ( ( `' A " NN ) i^i J ) C_ NN -> ( E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
87 85 86 mp1i 
 |-  ( A e. ( T i^i R ) -> ( E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p -> E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
88 82 87 impbid 
 |-  ( A e. ( T i^i R ) -> ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
89 38 88 bitr3d 
 |-  ( A e. ( T i^i R ) -> ( ( p e. NN /\ E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
90 eqeq2 
 |-  ( m = p -> ( ( ( 2 ^ n ) x. t ) = m <-> ( ( 2 ^ n ) x. t ) = p ) )
91 90 2rexbidv 
 |-  ( m = p -> ( E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m <-> E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
92 91 elrab 
 |-  ( p e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } <-> ( p e. NN /\ E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
93 92 a1i 
 |-  ( A e. ( T i^i R ) -> ( p e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } <-> ( p e. NN /\ E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) ) )
94 11 imaeq2i 
 |-  ( F " U ) = ( F " U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) )
95 imaiun 
 |-  ( F " U_ t e. ( ( `' A " NN ) i^i J ) ( { t } X. ( bits ` ( A ` t ) ) ) ) = U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. ( bits ` ( A ` t ) ) ) )
96 94 95 eqtri 
 |-  ( F " U ) = U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. ( bits ` ( A ` t ) ) ) )
97 96 eleq2i 
 |-  ( p e. ( F " U ) <-> p e. U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) )
98 eliun 
 |-  ( p e. U_ t e. ( ( `' A " NN ) i^i J ) ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) <-> E. t e. ( ( `' A " NN ) i^i J ) p e. ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) )
99 f1ofn 
 |-  ( F : ( J X. NN0 ) -1-1-onto-> NN -> F Fn ( J X. NN0 ) )
100 12 99 ax-mp 
 |-  F Fn ( J X. NN0 )
101 snssi 
 |-  ( t e. J -> { t } C_ J )
102 101 19 20 sylancl 
 |-  ( t e. J -> ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) )
103 ovelimab 
 |-  ( ( F Fn ( J X. NN0 ) /\ ( { t } X. ( bits ` ( A ` t ) ) ) C_ ( J X. NN0 ) ) -> ( p e. ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) <-> E. x e. { t } E. n e. ( bits ` ( A ` t ) ) p = ( x F n ) ) )
104 100 102 103 sylancr 
 |-  ( t e. J -> ( p e. ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) <-> E. x e. { t } E. n e. ( bits ` ( A ` t ) ) p = ( x F n ) ) )
105 vex 
 |-  t e. _V
106 oveq1 
 |-  ( x = t -> ( x F n ) = ( t F n ) )
107 106 eqeq2d 
 |-  ( x = t -> ( p = ( x F n ) <-> p = ( t F n ) ) )
108 107 rexbidv 
 |-  ( x = t -> ( E. n e. ( bits ` ( A ` t ) ) p = ( x F n ) <-> E. n e. ( bits ` ( A ` t ) ) p = ( t F n ) ) )
109 105 108 rexsn 
 |-  ( E. x e. { t } E. n e. ( bits ` ( A ` t ) ) p = ( x F n ) <-> E. n e. ( bits ` ( A ` t ) ) p = ( t F n ) )
110 104 109 bitrdi 
 |-  ( t e. J -> ( p e. ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) <-> E. n e. ( bits ` ( A ` t ) ) p = ( t F n ) ) )
111 df-ov 
 |-  ( t F n ) = ( F ` <. t , n >. )
112 111 eqeq1i 
 |-  ( ( t F n ) = p <-> ( F ` <. t , n >. ) = p )
113 eqcom 
 |-  ( ( t F n ) = p <-> p = ( t F n ) )
114 112 113 bitr3i 
 |-  ( ( F ` <. t , n >. ) = p <-> p = ( t F n ) )
115 opelxpi 
 |-  ( ( t e. J /\ n e. NN0 ) -> <. t , n >. e. ( J X. NN0 ) )
116 4 5 oddpwdcv 
 |-  ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) )
117 vex 
 |-  n e. _V
118 105 117 op2nd 
 |-  ( 2nd ` <. t , n >. ) = n
119 118 oveq2i 
 |-  ( 2 ^ ( 2nd ` <. t , n >. ) ) = ( 2 ^ n )
120 105 117 op1st 
 |-  ( 1st ` <. t , n >. ) = t
121 119 120 oveq12i 
 |-  ( ( 2 ^ ( 2nd ` <. t , n >. ) ) x. ( 1st ` <. t , n >. ) ) = ( ( 2 ^ n ) x. t )
122 116 121 eqtrdi 
 |-  ( <. t , n >. e. ( J X. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
123 115 122 syl 
 |-  ( ( t e. J /\ n e. NN0 ) -> ( F ` <. t , n >. ) = ( ( 2 ^ n ) x. t ) )
124 123 eqeq1d 
 |-  ( ( t e. J /\ n e. NN0 ) -> ( ( F ` <. t , n >. ) = p <-> ( ( 2 ^ n ) x. t ) = p ) )
125 114 124 bitr3id 
 |-  ( ( t e. J /\ n e. NN0 ) -> ( p = ( t F n ) <-> ( ( 2 ^ n ) x. t ) = p ) )
126 29 125 sylan2 
 |-  ( ( t e. J /\ n e. ( bits ` ( A ` t ) ) ) -> ( p = ( t F n ) <-> ( ( 2 ^ n ) x. t ) = p ) )
127 126 rexbidva 
 |-  ( t e. J -> ( E. n e. ( bits ` ( A ` t ) ) p = ( t F n ) <-> E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
128 110 127 bitrd 
 |-  ( t e. J -> ( p e. ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) <-> E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
129 17 128 syl 
 |-  ( t e. ( ( `' A " NN ) i^i J ) -> ( p e. ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) <-> E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
130 129 rexbiia 
 |-  ( E. t e. ( ( `' A " NN ) i^i J ) p e. ( F " ( { t } X. ( bits ` ( A ` t ) ) ) ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
131 97 98 130 3bitri 
 |-  ( p e. ( F " U ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p )
132 131 a1i 
 |-  ( A e. ( T i^i R ) -> ( p e. ( F " U ) <-> E. t e. ( ( `' A " NN ) i^i J ) E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = p ) )
133 89 93 132 3bitr4rd 
 |-  ( A e. ( T i^i R ) -> ( p e. ( F " U ) <-> p e. { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) )
134 133 eqrdv 
 |-  ( A e. ( T i^i R ) -> ( F " U ) = { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } )
135 f1oeq3 
 |-  ( ( F " U ) = { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } -> ( ( F |` U ) : U -1-1-onto-> ( F " U ) <-> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) )
136 134 135 syl 
 |-  ( A e. ( T i^i R ) -> ( ( F |` U ) : U -1-1-onto-> ( F " U ) <-> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } ) )
137 25 136 mpbii 
 |-  ( A e. ( T i^i R ) -> ( F |` U ) : U -1-1-onto-> { m e. NN | E. t e. NN E. n e. ( bits ` ( A ` t ) ) ( ( 2 ^ n ) x. t ) = m } )