Metamath Proof Explorer

Theorem sticksstones19

Description: Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024)

Ref Expression
Hypotheses sticksstones19.1 
|- ( ph -> N e. NN0 )
sticksstones19.2 
|- ( ph -> K e. NN0 )
sticksstones19.3 
|- A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
sticksstones19.4 
|- B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
sticksstones19.5 
|- ( ph -> Z : ( 1 ... K ) -1-1-onto-> S )
sticksstones19.6 
|- F = ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) )
sticksstones19.7 
|- G = ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) )
Assertion sticksstones19 
|- ( ph -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 sticksstones19.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones19.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones19.3 
 |-  A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
4 sticksstones19.4 
 |-  B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
5 sticksstones19.5 
 |-  ( ph -> Z : ( 1 ... K ) -1-1-onto-> S )
6 sticksstones19.6 
 |-  F = ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) )
7 sticksstones19.7 
 |-  G = ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) )
8 1 2 3 4 5 6 sticksstones18 
 |-  ( ph -> F : A --> B )
9 1 2 3 4 5 7 sticksstones17 
 |-  ( ph -> G : B --> A )
10 7 a1i 
 |-  ( ( ph /\ c e. A ) -> G = ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ) )
11 simplr 
 |-  ( ( ( ( ph /\ c e. A ) /\ b = ( F ` c ) ) /\ y e. ( 1 ... K ) ) -> b = ( F ` c ) )
12 11 fveq1d 
 |-  ( ( ( ( ph /\ c e. A ) /\ b = ( F ` c ) ) /\ y e. ( 1 ... K ) ) -> ( b ` ( Z ` y ) ) = ( ( F ` c ) ` ( Z ` y ) ) )
13 12 mpteq2dva 
 |-  ( ( ( ph /\ c e. A ) /\ b = ( F ` c ) ) -> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) = ( y e. ( 1 ... K ) |-> ( ( F ` c ) ` ( Z ` y ) ) ) )
14 8 ffvelrnda 
 |-  ( ( ph /\ c e. A ) -> ( F ` c ) e. B )
15 fzfid 
 |-  ( ( ph /\ c e. A ) -> ( 1 ... K ) e. Fin )
16 15 mptexd 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( ( F ` c ) ` ( Z ` y ) ) ) e. _V )
17 10 13 14 16 fvmptd 
 |-  ( ( ph /\ c e. A ) -> ( G ` ( F ` c ) ) = ( y e. ( 1 ... K ) |-> ( ( F ` c ) ` ( Z ` y ) ) ) )
18 6 a1i 
 |-  ( ( ph /\ c e. A /\ y e. ( 1 ... K ) ) -> F = ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) )
19 18 fveq1d 
 |-  ( ( ph /\ c e. A /\ y e. ( 1 ... K ) ) -> ( F ` c ) = ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) )
20 19 fveq1d 
 |-  ( ( ph /\ c e. A /\ y e. ( 1 ... K ) ) -> ( ( F ` c ) ` ( Z ` y ) ) = ( ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) ` ( Z ` y ) ) )
21 20 3expa 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( ( F ` c ) ` ( Z ` y ) ) = ( ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) ` ( Z ` y ) ) )
22 21 mpteq2dva 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( ( F ` c ) ` ( Z ` y ) ) ) = ( y e. ( 1 ... K ) |-> ( ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) ` ( Z ` y ) ) ) )
23 eqidd 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) = ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) )
24 simplr 
 |-  ( ( ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) /\ a = c ) /\ x e. S ) -> a = c )
25 24 fveq1d 
 |-  ( ( ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) /\ a = c ) /\ x e. S ) -> ( a ` ( `' Z ` x ) ) = ( c ` ( `' Z ` x ) ) )
26 25 mpteq2dva 
 |-  ( ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) /\ a = c ) -> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) = ( x e. S |-> ( c ` ( `' Z ` x ) ) ) )
27 simplr 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> c e. A )
28 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
29 f1oenfi 
 |-  ( ( ( 1 ... K ) e. Fin /\ Z : ( 1 ... K ) -1-1-onto-> S ) -> ( 1 ... K ) ~~ S )
30 28 5 29 syl2anc 
 |-  ( ph -> ( 1 ... K ) ~~ S )
31 30 ensymd 
 |-  ( ph -> S ~~ ( 1 ... K ) )
32 enfii 
 |-  ( ( ( 1 ... K ) e. Fin /\ S ~~ ( 1 ... K ) ) -> S e. Fin )
33 28 31 32 syl2anc 
 |-  ( ph -> S e. Fin )
34 33 adantr 
 |-  ( ( ph /\ c e. A ) -> S e. Fin )
35 34 adantr 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> S e. Fin )
36 35 mptexd 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( x e. S |-> ( c ` ( `' Z ` x ) ) ) e. _V )
37 23 26 27 36 fvmptd 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) = ( x e. S |-> ( c ` ( `' Z ` x ) ) ) )
38 37 fveq1d 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) ` ( Z ` y ) ) = ( ( x e. S |-> ( c ` ( `' Z ` x ) ) ) ` ( Z ` y ) ) )
39 38 mpteq2dva 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) ` ( Z ` y ) ) ) = ( y e. ( 1 ... K ) |-> ( ( x e. S |-> ( c ` ( `' Z ` x ) ) ) ` ( Z ` y ) ) ) )
40 eqidd 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( x e. S |-> ( c ` ( `' Z ` x ) ) ) = ( x e. S |-> ( c ` ( `' Z ` x ) ) ) )
41 simpr 
 |-  ( ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) /\ x = ( Z ` y ) ) -> x = ( Z ` y ) )
42 41 fveq2d 
 |-  ( ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) /\ x = ( Z ` y ) ) -> ( `' Z ` x ) = ( `' Z ` ( Z ` y ) ) )
43 42 fveq2d 
 |-  ( ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) /\ x = ( Z ` y ) ) -> ( c ` ( `' Z ` x ) ) = ( c ` ( `' Z ` ( Z ` y ) ) ) )
44 f1of 
 |-  ( Z : ( 1 ... K ) -1-1-onto-> S -> Z : ( 1 ... K ) --> S )
45 5 44 syl 
 |-  ( ph -> Z : ( 1 ... K ) --> S )
46 45 adantr 
 |-  ( ( ph /\ c e. A ) -> Z : ( 1 ... K ) --> S )
47 46 ffvelrnda 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( Z ` y ) e. S )
48 fvexd 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( c ` ( `' Z ` ( Z ` y ) ) ) e. _V )
49 40 43 47 48 fvmptd 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( ( x e. S |-> ( c ` ( `' Z ` x ) ) ) ` ( Z ` y ) ) = ( c ` ( `' Z ` ( Z ` y ) ) ) )
50 49 mpteq2dva 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( ( x e. S |-> ( c ` ( `' Z ` x ) ) ) ` ( Z ` y ) ) ) = ( y e. ( 1 ... K ) |-> ( c ` ( `' Z ` ( Z ` y ) ) ) ) )
51 5 ad2antrr 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> Z : ( 1 ... K ) -1-1-onto-> S )
52 simpr 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> y e. ( 1 ... K ) )
53 f1ocnvfv1 
 |-  ( ( Z : ( 1 ... K ) -1-1-onto-> S /\ y e. ( 1 ... K ) ) -> ( `' Z ` ( Z ` y ) ) = y )
54 51 52 53 syl2anc 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( `' Z ` ( Z ` y ) ) = y )
55 54 fveq2d 
 |-  ( ( ( ph /\ c e. A ) /\ y e. ( 1 ... K ) ) -> ( c ` ( `' Z ` ( Z ` y ) ) ) = ( c ` y ) )
56 55 mpteq2dva 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( c ` ( `' Z ` ( Z ` y ) ) ) ) = ( y e. ( 1 ... K ) |-> ( c ` y ) ) )
57 simpr 
 |-  ( ( ph /\ c e. A ) -> c e. A )
58 3 a1i 
 |-  ( ( ph /\ c e. A ) -> A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } )
59 57 58 eleqtrd 
 |-  ( ( ph /\ c e. A ) -> c e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } )
60 vex 
 |-  c e. _V
61 feq1 
 |-  ( g = c -> ( g : ( 1 ... K ) --> NN0 <-> c : ( 1 ... K ) --> NN0 ) )
62 simpl 
 |-  ( ( g = c /\ i e. ( 1 ... K ) ) -> g = c )
63 62 fveq1d 
 |-  ( ( g = c /\ i e. ( 1 ... K ) ) -> ( g ` i ) = ( c ` i ) )
64 63 sumeq2dv 
 |-  ( g = c -> sum_ i e. ( 1 ... K ) ( g ` i ) = sum_ i e. ( 1 ... K ) ( c ` i ) )
65 64 eqeq1d 
 |-  ( g = c -> ( sum_ i e. ( 1 ... K ) ( g ` i ) = N <-> sum_ i e. ( 1 ... K ) ( c ` i ) = N ) )
66 61 65 anbi12d 
 |-  ( g = c -> ( ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) <-> ( c : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( c ` i ) = N ) ) )
67 60 66 elab 
 |-  ( c e. { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } <-> ( c : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( c ` i ) = N ) )
68 59 67 sylib 
 |-  ( ( ph /\ c e. A ) -> ( c : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( c ` i ) = N ) )
69 68 simpld 
 |-  ( ( ph /\ c e. A ) -> c : ( 1 ... K ) --> NN0 )
70 ffn 
 |-  ( c : ( 1 ... K ) --> NN0 -> c Fn ( 1 ... K ) )
71 69 70 syl 
 |-  ( ( ph /\ c e. A ) -> c Fn ( 1 ... K ) )
72 dffn5 
 |-  ( c Fn ( 1 ... K ) <-> c = ( y e. ( 1 ... K ) |-> ( c ` y ) ) )
73 71 72 sylib 
 |-  ( ( ph /\ c e. A ) -> c = ( y e. ( 1 ... K ) |-> ( c ` y ) ) )
74 73 eqcomd 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( c ` y ) ) = c )
75 56 74 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( c ` ( `' Z ` ( Z ` y ) ) ) ) = c )
76 50 75 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( ( x e. S |-> ( c ` ( `' Z ` x ) ) ) ` ( Z ` y ) ) ) = c )
77 39 76 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( ( ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) ` c ) ` ( Z ` y ) ) ) = c )
78 22 77 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( y e. ( 1 ... K ) |-> ( ( F ` c ) ` ( Z ` y ) ) ) = c )
79 17 78 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( G ` ( F ` c ) ) = c )
80 79 ralrimiva 
 |-  ( ph -> A. c e. A ( G ` ( F ` c ) ) = c )
81 6 a1i 
 |-  ( ( ph /\ d e. B ) -> F = ( a e. A |-> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) ) )
82 simplr 
 |-  ( ( ( ( ph /\ d e. B ) /\ a = ( G ` d ) ) /\ x e. S ) -> a = ( G ` d ) )
83 82 fveq1d 
 |-  ( ( ( ( ph /\ d e. B ) /\ a = ( G ` d ) ) /\ x e. S ) -> ( a ` ( `' Z ` x ) ) = ( ( G ` d ) ` ( `' Z ` x ) ) )
84 83 mpteq2dva 
 |-  ( ( ( ph /\ d e. B ) /\ a = ( G ` d ) ) -> ( x e. S |-> ( a ` ( `' Z ` x ) ) ) = ( x e. S |-> ( ( G ` d ) ` ( `' Z ` x ) ) ) )
85 9 ffvelrnda 
 |-  ( ( ph /\ d e. B ) -> ( G ` d ) e. A )
86 33 adantr 
 |-  ( ( ph /\ d e. B ) -> S e. Fin )
87 86 mptexd 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( ( G ` d ) ` ( `' Z ` x ) ) ) e. _V )
88 81 84 85 87 fvmptd 
 |-  ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = ( x e. S |-> ( ( G ` d ) ` ( `' Z ` x ) ) ) )
89 7 a1i 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> G = ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) ) )
90 simplr 
 |-  ( ( ( ( ( ph /\ d e. B ) /\ x e. S ) /\ b = d ) /\ y e. ( 1 ... K ) ) -> b = d )
91 90 fveq1d 
 |-  ( ( ( ( ( ph /\ d e. B ) /\ x e. S ) /\ b = d ) /\ y e. ( 1 ... K ) ) -> ( b ` ( Z ` y ) ) = ( d ` ( Z ` y ) ) )
92 91 mpteq2dva 
 |-  ( ( ( ( ph /\ d e. B ) /\ x e. S ) /\ b = d ) -> ( y e. ( 1 ... K ) |-> ( b ` ( Z ` y ) ) ) = ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) )
93 simplr 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> d e. B )
94 fzfid 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( 1 ... K ) e. Fin )
95 94 mptexd 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) e. _V )
96 89 92 93 95 fvmptd 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( G ` d ) = ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) )
97 96 fveq1d 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( ( G ` d ) ` ( `' Z ` x ) ) = ( ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) ` ( `' Z ` x ) ) )
98 97 mpteq2dva 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( ( G ` d ) ` ( `' Z ` x ) ) ) = ( x e. S |-> ( ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) ` ( `' Z ` x ) ) ) )
99 eqidd 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) = ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) )
100 simpr 
 |-  ( ( ( ( ph /\ d e. B ) /\ x e. S ) /\ y = ( `' Z ` x ) ) -> y = ( `' Z ` x ) )
101 100 fveq2d 
 |-  ( ( ( ( ph /\ d e. B ) /\ x e. S ) /\ y = ( `' Z ` x ) ) -> ( Z ` y ) = ( Z ` ( `' Z ` x ) ) )
102 101 fveq2d 
 |-  ( ( ( ( ph /\ d e. B ) /\ x e. S ) /\ y = ( `' Z ` x ) ) -> ( d ` ( Z ` y ) ) = ( d ` ( Z ` ( `' Z ` x ) ) ) )
103 f1ocnv 
 |-  ( Z : ( 1 ... K ) -1-1-onto-> S -> `' Z : S -1-1-onto-> ( 1 ... K ) )
104 5 103 syl 
 |-  ( ph -> `' Z : S -1-1-onto-> ( 1 ... K ) )
105 f1of 
 |-  ( `' Z : S -1-1-onto-> ( 1 ... K ) -> `' Z : S --> ( 1 ... K ) )
106 104 105 syl 
 |-  ( ph -> `' Z : S --> ( 1 ... K ) )
107 106 adantr 
 |-  ( ( ph /\ d e. B ) -> `' Z : S --> ( 1 ... K ) )
108 107 ffvelrnda 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( `' Z ` x ) e. ( 1 ... K ) )
109 fvexd 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( d ` ( Z ` ( `' Z ` x ) ) ) e. _V )
110 99 102 108 109 fvmptd 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) ` ( `' Z ` x ) ) = ( d ` ( Z ` ( `' Z ` x ) ) ) )
111 110 mpteq2dva 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) ` ( `' Z ` x ) ) ) = ( x e. S |-> ( d ` ( Z ` ( `' Z ` x ) ) ) ) )
112 5 ad2antrr 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> Z : ( 1 ... K ) -1-1-onto-> S )
113 simpr 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> x e. S )
114 f1ocnvfv2 
 |-  ( ( Z : ( 1 ... K ) -1-1-onto-> S /\ x e. S ) -> ( Z ` ( `' Z ` x ) ) = x )
115 112 113 114 syl2anc 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( Z ` ( `' Z ` x ) ) = x )
116 115 fveq2d 
 |-  ( ( ( ph /\ d e. B ) /\ x e. S ) -> ( d ` ( Z ` ( `' Z ` x ) ) ) = ( d ` x ) )
117 116 mpteq2dva 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( d ` ( Z ` ( `' Z ` x ) ) ) ) = ( x e. S |-> ( d ` x ) ) )
118 simpr 
 |-  ( ( ph /\ d e. B ) -> d e. B )
119 4 a1i 
 |-  ( ( ph /\ d e. B ) -> B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } )
120 118 119 eleqtrd 
 |-  ( ( ph /\ d e. B ) -> d e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } )
121 vex 
 |-  d e. _V
122 feq1 
 |-  ( h = d -> ( h : S --> NN0 <-> d : S --> NN0 ) )
123 simpl 
 |-  ( ( h = d /\ i e. S ) -> h = d )
124 123 fveq1d 
 |-  ( ( h = d /\ i e. S ) -> ( h ` i ) = ( d ` i ) )
125 124 sumeq2dv 
 |-  ( h = d -> sum_ i e. S ( h ` i ) = sum_ i e. S ( d ` i ) )
126 125 eqeq1d 
 |-  ( h = d -> ( sum_ i e. S ( h ` i ) = N <-> sum_ i e. S ( d ` i ) = N ) )
127 122 126 anbi12d 
 |-  ( h = d -> ( ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) <-> ( d : S --> NN0 /\ sum_ i e. S ( d ` i ) = N ) ) )
128 121 127 elab 
 |-  ( d e. { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) } <-> ( d : S --> NN0 /\ sum_ i e. S ( d ` i ) = N ) )
129 120 128 sylib 
 |-  ( ( ph /\ d e. B ) -> ( d : S --> NN0 /\ sum_ i e. S ( d ` i ) = N ) )
130 129 simpld 
 |-  ( ( ph /\ d e. B ) -> d : S --> NN0 )
131 ffn 
 |-  ( d : S --> NN0 -> d Fn S )
132 130 131 syl 
 |-  ( ( ph /\ d e. B ) -> d Fn S )
133 dffn5 
 |-  ( d Fn S <-> d = ( x e. S |-> ( d ` x ) ) )
134 132 133 sylib 
 |-  ( ( ph /\ d e. B ) -> d = ( x e. S |-> ( d ` x ) ) )
135 134 eqcomd 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( d ` x ) ) = d )
136 117 135 eqtrd 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( d ` ( Z ` ( `' Z ` x ) ) ) ) = d )
137 111 136 eqtrd 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( ( y e. ( 1 ... K ) |-> ( d ` ( Z ` y ) ) ) ` ( `' Z ` x ) ) ) = d )
138 98 137 eqtrd 
 |-  ( ( ph /\ d e. B ) -> ( x e. S |-> ( ( G ` d ) ` ( `' Z ` x ) ) ) = d )
139 88 138 eqtrd 
 |-  ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = d )
140 139 ralrimiva 
 |-  ( ph -> A. d e. B ( F ` ( G ` d ) ) = d )
141 8 9 80 140 2fvidf1od 
 |-  ( ph -> F : A -1-1-onto-> B )