Metamath Proof Explorer

Theorem sticksstones11

Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024)

Ref Expression
Hypotheses sticksstones11.1 
|- ( ph -> N e. NN0 )
sticksstones11.2 
|- ( ph -> K = 0 )
sticksstones11.3 
|- F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
sticksstones11.4 
|- G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
sticksstones11.5 
|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
sticksstones11.6 
|- B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
Assertion sticksstones11 
|- ( ph -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 sticksstones11.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones11.2 
 |-  ( ph -> K = 0 )
3 sticksstones11.3 
 |-  F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
4 sticksstones11.4 
 |-  G = ( b e. B |-> if ( K = 0 , { <. 1 , N >. } , ( k e. ( 1 ... ( K + 1 ) ) |-> if ( k = ( K + 1 ) , ( ( N + K ) - ( b ` K ) ) , if ( k = 1 , ( ( b ` 1 ) - 1 ) , ( ( ( b ` k ) - ( b ` ( k - 1 ) ) ) - 1 ) ) ) ) ) )
5 sticksstones11.5 
 |-  A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
6 sticksstones11.6 
 |-  B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
7 0nn0 
 |-  0 e. NN0
8 7 a1i 
 |-  ( ph -> 0 e. NN0 )
9 2 8 eqeltrd 
 |-  ( ph -> K e. NN0 )
10 1 9 3 5 6 sticksstones8 
 |-  ( ph -> F : A --> B )
11 1 2 4 5 6 sticksstones9 
 |-  ( ph -> G : B --> A )
12 5 a1i 
 |-  ( ph -> A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
13 nfv 
 |-  F/ u ph
14 nfcv 
 |-  F/_ u { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
15 nfcv 
 |-  F/_ u { { <. 1 , N >. } }
16 ffn 
 |-  ( u : { 1 } --> NN0 -> u Fn { 1 } )
17 16 ad2antrl 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u Fn { 1 } )
18 1nn 
 |-  1 e. NN
19 18 a1i 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> 1 e. NN )
20 1 adantr 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> N e. NN0 )
21 fnsng 
 |-  ( ( 1 e. NN /\ N e. NN0 ) -> { <. 1 , N >. } Fn { 1 } )
22 19 20 21 syl2anc 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> { <. 1 , N >. } Fn { 1 } )
23 elsni 
 |-  ( p e. { 1 } -> p = 1 )
24 23 adantl 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> p = 1 )
25 simpr 
 |-  ( ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) /\ p = 1 ) -> p = 1 )
26 25 fveq2d 
 |-  ( ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) /\ p = 1 ) -> ( u ` p ) = ( u ` 1 ) )
27 simprl 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u : { 1 } --> NN0 )
28 1ex 
 |-  1 e. _V
29 28 snid 
 |-  1 e. { 1 }
30 29 a1i 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> 1 e. { 1 } )
31 27 30 ffvelrnd 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> ( u ` 1 ) e. NN0 )
32 31 nn0cnd 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> ( u ` 1 ) e. CC )
33 fveq2 
 |-  ( i = 1 -> ( u ` i ) = ( u ` 1 ) )
34 33 sumsn 
 |-  ( ( 1 e. NN /\ ( u ` 1 ) e. CC ) -> sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) )
35 19 32 34 syl2anc 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) )
36 35 adantr 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) ) -> sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) )
37 36 eqcomd 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) ) -> ( u ` 1 ) = sum_ i e. { 1 } ( u ` i ) )
38 simplrr 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) ) -> sum_ i e. { 1 } ( u ` i ) = N )
39 37 38 eqtrd 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) ) -> ( u ` 1 ) = N )
40 39 ex 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> ( sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) -> ( u ` 1 ) = N ) )
41 35 40 mpd 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> ( u ` 1 ) = N )
42 41 adantr 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> ( u ` 1 ) = N )
43 18 a1i 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> 1 e. NN )
44 20 adantr 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> N e. NN0 )
45 fvsng 
 |-  ( ( 1 e. NN /\ N e. NN0 ) -> ( { <. 1 , N >. } ` 1 ) = N )
46 43 44 45 syl2anc 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> ( { <. 1 , N >. } ` 1 ) = N )
47 46 eqcomd 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> N = ( { <. 1 , N >. } ` 1 ) )
48 42 47 eqtrd 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> ( u ` 1 ) = ( { <. 1 , N >. } ` 1 ) )
49 48 adantr 
 |-  ( ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) /\ p = 1 ) -> ( u ` 1 ) = ( { <. 1 , N >. } ` 1 ) )
50 25 eqcomd 
 |-  ( ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) /\ p = 1 ) -> 1 = p )
51 50 fveq2d 
 |-  ( ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) /\ p = 1 ) -> ( { <. 1 , N >. } ` 1 ) = ( { <. 1 , N >. } ` p ) )
52 26 49 51 3eqtrd 
 |-  ( ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) /\ p = 1 ) -> ( u ` p ) = ( { <. 1 , N >. } ` p ) )
53 24 52 mpdan 
 |-  ( ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) /\ p e. { 1 } ) -> ( u ` p ) = ( { <. 1 , N >. } ` p ) )
54 17 22 53 eqfnfvd 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u = { <. 1 , N >. } )
55 fsng 
 |-  ( ( 1 e. NN /\ N e. NN0 ) -> ( u : { 1 } --> { N } <-> u = { <. 1 , N >. } ) )
56 19 20 55 syl2anc 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> ( u : { 1 } --> { N } <-> u = { <. 1 , N >. } ) )
57 54 56 mpbird 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u : { 1 } --> { N } )
58 ssidd 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> { N } C_ { N } )
59 fss 
 |-  ( ( u : { 1 } --> { N } /\ { N } C_ { N } ) -> u : { 1 } --> { N } )
60 57 58 59 syl2anc 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u : { 1 } --> { N } )
61 60 58 59 syl2anc 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u : { 1 } --> { N } )
62 61 56 mpbid 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u = { <. 1 , N >. } )
63 vex 
 |-  u e. _V
64 63 elsn 
 |-  ( u e. { { <. 1 , N >. } } <-> u = { <. 1 , N >. } )
65 62 64 sylibr 
 |-  ( ( ph /\ ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) ) -> u e. { { <. 1 , N >. } } )
66 65 ex 
 |-  ( ph -> ( ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) -> u e. { { <. 1 , N >. } } ) )
67 1zzd 
 |-  ( ph -> 1 e. ZZ )
68 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
69 67 68 syl 
 |-  ( ph -> ( 1 ... 1 ) = { 1 } )
70 69 eqcomd 
 |-  ( ph -> { 1 } = ( 1 ... 1 ) )
71 1e0p1 
 |-  1 = ( 0 + 1 )
72 71 a1i 
 |-  ( ph -> 1 = ( 0 + 1 ) )
73 72 oveq2d 
 |-  ( ph -> ( 1 ... 1 ) = ( 1 ... ( 0 + 1 ) ) )
74 70 73 eqtrd 
 |-  ( ph -> { 1 } = ( 1 ... ( 0 + 1 ) ) )
75 2 eqcomd 
 |-  ( ph -> 0 = K )
76 75 oveq1d 
 |-  ( ph -> ( 0 + 1 ) = ( K + 1 ) )
77 76 oveq2d 
 |-  ( ph -> ( 1 ... ( 0 + 1 ) ) = ( 1 ... ( K + 1 ) ) )
78 74 77 eqtrd 
 |-  ( ph -> { 1 } = ( 1 ... ( K + 1 ) ) )
79 78 feq2d 
 |-  ( ph -> ( u : { 1 } --> NN0 <-> u : ( 1 ... ( K + 1 ) ) --> NN0 ) )
80 78 sumeq1d 
 |-  ( ph -> sum_ i e. { 1 } ( u ` i ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) )
81 80 eqeq1d 
 |-  ( ph -> ( sum_ i e. { 1 } ( u ` i ) = N <-> sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) )
82 79 81 anbi12d 
 |-  ( ph -> ( ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) <-> ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) ) )
83 82 imbi1d 
 |-  ( ph -> ( ( ( u : { 1 } --> NN0 /\ sum_ i e. { 1 } ( u ` i ) = N ) -> u e. { { <. 1 , N >. } } ) <-> ( ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) -> u e. { { <. 1 , N >. } } ) ) )
84 66 83 mpbid 
 |-  ( ph -> ( ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) -> u e. { { <. 1 , N >. } } ) )
85 feq1 
 |-  ( g = u -> ( g : ( 1 ... ( K + 1 ) ) --> NN0 <-> u : ( 1 ... ( K + 1 ) ) --> NN0 ) )
86 simpl 
 |-  ( ( g = u /\ i e. ( 1 ... ( K + 1 ) ) ) -> g = u )
87 86 fveq1d 
 |-  ( ( g = u /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( g ` i ) = ( u ` i ) )
88 87 sumeq2dv 
 |-  ( g = u -> sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) )
89 88 eqeq1d 
 |-  ( g = u -> ( sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N <-> sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) )
90 85 89 anbi12d 
 |-  ( g = u -> ( ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) <-> ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) ) )
91 63 90 elab 
 |-  ( u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) )
92 91 a1i 
 |-  ( ph -> ( u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } <-> ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) ) )
93 92 imbi1d 
 |-  ( ph -> ( ( u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } -> u e. { { <. 1 , N >. } } ) <-> ( ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) -> u e. { { <. 1 , N >. } } ) ) )
94 84 93 mpbird 
 |-  ( ph -> ( u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } -> u e. { { <. 1 , N >. } } ) )
95 94 imp 
 |-  ( ( ph /\ u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } ) -> u e. { { <. 1 , N >. } } )
96 95 ex 
 |-  ( ph -> ( u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } -> u e. { { <. 1 , N >. } } ) )
97 13 14 15 96 ssrd 
 |-  ( ph -> { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } C_ { { <. 1 , N >. } } )
98 18 a1i 
 |-  ( ph -> 1 e. NN )
99 98 1 55 syl2anc 
 |-  ( ph -> ( u : { 1 } --> { N } <-> u = { <. 1 , N >. } ) )
100 99 bicomd 
 |-  ( ph -> ( u = { <. 1 , N >. } <-> u : { 1 } --> { N } ) )
101 100 biimpd 
 |-  ( ph -> ( u = { <. 1 , N >. } -> u : { 1 } --> { N } ) )
102 elsni 
 |-  ( u e. { { <. 1 , N >. } } -> u = { <. 1 , N >. } )
103 101 102 impel 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> u : { 1 } --> { N } )
104 1 snssd 
 |-  ( ph -> { N } C_ NN0 )
105 104 adantr 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> { N } C_ NN0 )
106 fss 
 |-  ( ( u : { 1 } --> { N } /\ { N } C_ NN0 ) -> u : { 1 } --> NN0 )
107 103 105 106 syl2anc 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> u : { 1 } --> NN0 )
108 79 adantr 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> ( u : { 1 } --> NN0 <-> u : ( 1 ... ( K + 1 ) ) --> NN0 ) )
109 107 108 mpbid 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> u : ( 1 ... ( K + 1 ) ) --> NN0 )
110 102 adantl 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> u = { <. 1 , N >. } )
111 78 3ad2ant1 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> { 1 } = ( 1 ... ( K + 1 ) ) )
112 111 eqcomd 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> ( 1 ... ( K + 1 ) ) = { 1 } )
113 112 sumeq1d 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = sum_ i e. { 1 } ( u ` i ) )
114 18 a1i 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> 1 e. NN )
115 1 3ad2ant1 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> N e. NN0 )
116 115 nn0cnd 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> N e. CC )
117 114 115 45 syl2anc 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> ( { <. 1 , N >. } ` 1 ) = N )
118 117 eqcomd 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> N = ( { <. 1 , N >. } ` 1 ) )
119 110 3adant3 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> u = { <. 1 , N >. } )
120 119 fveq1d 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> ( u ` 1 ) = ( { <. 1 , N >. } ` 1 ) )
121 118 120 eqtr4d 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> N = ( u ` 1 ) )
122 121 eleq1d 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> ( N e. CC <-> ( u ` 1 ) e. CC ) )
123 116 122 mpbid 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> ( u ` 1 ) e. CC )
124 114 123 34 syl2anc 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> sum_ i e. { 1 } ( u ` i ) = ( u ` 1 ) )
125 120 117 eqtrd 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> ( u ` 1 ) = N )
126 124 125 eqtrd 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> sum_ i e. { 1 } ( u ` i ) = N )
127 113 126 eqtrd 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } /\ u = { <. 1 , N >. } ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N )
128 127 3expa 
 |-  ( ( ( ph /\ u e. { { <. 1 , N >. } } ) /\ u = { <. 1 , N >. } ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N )
129 110 128 mpdan 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N )
130 109 129 jca 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> ( u : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( u ` i ) = N ) )
131 130 91 sylibr 
 |-  ( ( ph /\ u e. { { <. 1 , N >. } } ) -> u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
132 131 ex 
 |-  ( ph -> ( u e. { { <. 1 , N >. } } -> u e. { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } ) )
133 13 15 14 132 ssrd 
 |-  ( ph -> { { <. 1 , N >. } } C_ { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
134 97 133 eqssd 
 |-  ( ph -> { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } = { { <. 1 , N >. } } )
135 12 134 eqtrd 
 |-  ( ph -> A = { { <. 1 , N >. } } )
136 eqss 
 |-  ( A = { { <. 1 , N >. } } <-> ( A C_ { { <. 1 , N >. } } /\ { { <. 1 , N >. } } C_ A ) )
137 136 biimpi 
 |-  ( A = { { <. 1 , N >. } } -> ( A C_ { { <. 1 , N >. } } /\ { { <. 1 , N >. } } C_ A ) )
138 137 simpld 
 |-  ( A = { { <. 1 , N >. } } -> A C_ { { <. 1 , N >. } } )
139 135 138 syl 
 |-  ( ph -> A C_ { { <. 1 , N >. } } )
140 fss 
 |-  ( ( G : B --> A /\ A C_ { { <. 1 , N >. } } ) -> G : B --> { { <. 1 , N >. } } )
141 11 139 140 syl2anc 
 |-  ( ph -> G : B --> { { <. 1 , N >. } } )
142 141 adantr 
 |-  ( ( ph /\ c e. A ) -> G : B --> { { <. 1 , N >. } } )
143 10 ffvelrnda 
 |-  ( ( ph /\ c e. A ) -> ( F ` c ) e. B )
144 fvconst 
 |-  ( ( G : B --> { { <. 1 , N >. } } /\ ( F ` c ) e. B ) -> ( G ` ( F ` c ) ) = { <. 1 , N >. } )
145 142 143 144 syl2anc 
 |-  ( ( ph /\ c e. A ) -> ( G ` ( F ` c ) ) = { <. 1 , N >. } )
146 135 eleq2d 
 |-  ( ph -> ( c e. A <-> c e. { { <. 1 , N >. } } ) )
147 146 biimpd 
 |-  ( ph -> ( c e. A -> c e. { { <. 1 , N >. } } ) )
148 147 imp 
 |-  ( ( ph /\ c e. A ) -> c e. { { <. 1 , N >. } } )
149 vex 
 |-  c e. _V
150 149 elsn 
 |-  ( c e. { { <. 1 , N >. } } <-> c = { <. 1 , N >. } )
151 148 150 sylib 
 |-  ( ( ph /\ c e. A ) -> c = { <. 1 , N >. } )
152 151 eqcomd 
 |-  ( ( ph /\ c e. A ) -> { <. 1 , N >. } = c )
153 145 152 eqtrd 
 |-  ( ( ph /\ c e. A ) -> ( G ` ( F ` c ) ) = c )
154 153 ralrimiva 
 |-  ( ph -> A. c e. A ( G ` ( F ` c ) ) = c )
155 simpr 
 |-  ( ( ph /\ d e. B ) -> d e. B )
156 nfv 
 |-  F/ d ph
157 nfcv 
 |-  F/_ d B
158 nfcv 
 |-  F/_ d { (/) }
159 6 a1i 
 |-  ( ( ph /\ d e. B ) -> B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
160 159 eleq2d 
 |-  ( ( ph /\ d e. B ) -> ( d e. B <-> d e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } ) )
161 160 biimpd 
 |-  ( ( ph /\ d e. B ) -> ( d e. B -> d e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } ) )
162 161 syldbl2 
 |-  ( ( ph /\ d e. B ) -> d e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
163 vex 
 |-  d e. _V
164 feq1 
 |-  ( f = d -> ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) ) )
165 fveq1 
 |-  ( f = d -> ( f ` x ) = ( d ` x ) )
166 fveq1 
 |-  ( f = d -> ( f ` y ) = ( d ` y ) )
167 165 166 breq12d 
 |-  ( f = d -> ( ( f ` x ) < ( f ` y ) <-> ( d ` x ) < ( d ` y ) ) )
168 167 imbi2d 
 |-  ( f = d -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
169 168 2ralbidv 
 |-  ( f = d -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) <-> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
170 164 169 anbi12d 
 |-  ( f = d -> ( ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) ) )
171 163 170 elab 
 |-  ( d e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } <-> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
172 162 171 sylib 
 |-  ( ( ph /\ d e. B ) -> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( d ` x ) < ( d ` y ) ) ) )
173 172 simpld 
 |-  ( ( ph /\ d e. B ) -> d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
174 0lt1 
 |-  0 < 1
175 174 a1i 
 |-  ( ph -> 0 < 1 )
176 2 175 eqbrtrd 
 |-  ( ph -> K < 1 )
177 9 nn0zd 
 |-  ( ph -> K e. ZZ )
178 fzn 
 |-  ( ( 1 e. ZZ /\ K e. ZZ ) -> ( K < 1 <-> ( 1 ... K ) = (/) ) )
179 67 177 178 syl2anc 
 |-  ( ph -> ( K < 1 <-> ( 1 ... K ) = (/) ) )
180 176 179 mpbid 
 |-  ( ph -> ( 1 ... K ) = (/) )
181 180 feq2d 
 |-  ( ph -> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> d : (/) --> ( 1 ... ( N + K ) ) ) )
182 181 adantr 
 |-  ( ( ph /\ d e. B ) -> ( d : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> d : (/) --> ( 1 ... ( N + K ) ) ) )
183 173 182 mpbid 
 |-  ( ( ph /\ d e. B ) -> d : (/) --> ( 1 ... ( N + K ) ) )
184 f0bi 
 |-  ( d : (/) --> ( 1 ... ( N + K ) ) <-> d = (/) )
185 183 184 sylib 
 |-  ( ( ph /\ d e. B ) -> d = (/) )
186 velsn 
 |-  ( d e. { (/) } <-> d = (/) )
187 185 186 sylibr 
 |-  ( ( ph /\ d e. B ) -> d e. { (/) } )
188 187 ex 
 |-  ( ph -> ( d e. B -> d e. { (/) } ) )
189 f0 
 |-  (/) : (/) --> ( 1 ... ( N + K ) )
190 189 a1i 
 |-  ( ph -> (/) : (/) --> ( 1 ... ( N + K ) ) )
191 180 feq2d 
 |-  ( ph -> ( (/) : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> (/) : (/) --> ( 1 ... ( N + K ) ) ) )
192 190 191 mpbird 
 |-  ( ph -> (/) : ( 1 ... K ) --> ( 1 ... ( N + K ) ) )
193 ral0 
 |-  A. x e. (/) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) )
194 193 a1i 
 |-  ( ph -> A. x e. (/) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) )
195 biidd 
 |-  ( ( ph /\ x e. ( 1 ... K ) ) -> ( A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) <-> A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) )
196 180 195 raleqbidva 
 |-  ( ph -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) <-> A. x e. (/) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) )
197 194 196 mpbird 
 |-  ( ph -> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) )
198 192 197 jca 
 |-  ( ph -> ( (/) : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) )
199 0ex 
 |-  (/) e. _V
200 feq1 
 |-  ( f = (/) -> ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> (/) : ( 1 ... K ) --> ( 1 ... ( N + K ) ) ) )
201 fveq1 
 |-  ( f = (/) -> ( f ` x ) = ( (/) ` x ) )
202 fveq1 
 |-  ( f = (/) -> ( f ` y ) = ( (/) ` y ) )
203 201 202 breq12d 
 |-  ( f = (/) -> ( ( f ` x ) < ( f ` y ) <-> ( (/) ` x ) < ( (/) ` y ) ) )
204 203 imbi2d 
 |-  ( f = (/) -> ( ( x < y -> ( f ` x ) < ( f ` y ) ) <-> ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) )
205 204 2ralbidv 
 |-  ( f = (/) -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) <-> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) )
206 200 205 anbi12d 
 |-  ( f = (/) -> ( ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) <-> ( (/) : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) ) )
207 206 elabg 
 |-  ( (/) e. _V -> ( (/) e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } <-> ( (/) : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) ) )
208 199 207 ax-mp 
 |-  ( (/) e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } <-> ( (/) : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( (/) ` x ) < ( (/) ` y ) ) ) )
209 198 208 sylibr 
 |-  ( ph -> (/) e. { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
210 6 a1i 
 |-  ( ph -> B = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) } )
211 209 210 eleqtrrd 
 |-  ( ph -> (/) e. B )
212 211 adantr 
 |-  ( ( ph /\ d e. { (/) } ) -> (/) e. B )
213 elsni 
 |-  ( d e. { (/) } -> d = (/) )
214 213 adantl 
 |-  ( ( ph /\ d e. { (/) } ) -> d = (/) )
215 214 eleq1d 
 |-  ( ( ph /\ d e. { (/) } ) -> ( d e. B <-> (/) e. B ) )
216 212 215 mpbird 
 |-  ( ( ph /\ d e. { (/) } ) -> d e. B )
217 216 ex 
 |-  ( ph -> ( d e. { (/) } -> d e. B ) )
218 188 217 impbid 
 |-  ( ph -> ( d e. B <-> d e. { (/) } ) )
219 156 157 158 218 eqrd 
 |-  ( ph -> B = { (/) } )
220 219 adantr 
 |-  ( ( ph /\ d e. B ) -> B = { (/) } )
221 155 220 eleqtrd 
 |-  ( ( ph /\ d e. B ) -> d e. { (/) } )
222 163 elsn 
 |-  ( d e. { (/) } <-> d = (/) )
223 221 222 sylib 
 |-  ( ( ph /\ d e. B ) -> d = (/) )
224 223 fveq2d 
 |-  ( ( ph /\ d e. B ) -> ( G ` d ) = ( G ` (/) ) )
225 224 fveq2d 
 |-  ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = ( F ` ( G ` (/) ) ) )
226 180 adantr 
 |-  ( ( ph /\ a e. A ) -> ( 1 ... K ) = (/) )
227 226 mpteq1d 
 |-  ( ( ph /\ a e. A ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = ( j e. (/) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
228 mpt0 
 |-  ( j e. (/) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = (/)
229 228 a1i 
 |-  ( ( ph /\ a e. A ) -> ( j e. (/) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = (/) )
230 227 229 eqtrd 
 |-  ( ( ph /\ a e. A ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = (/) )
231 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
232 231 mptexd 
 |-  ( ph -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) e. _V )
233 elsng 
 |-  ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) e. _V -> ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) e. { (/) } <-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = (/) ) )
234 232 233 syl 
 |-  ( ph -> ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) e. { (/) } <-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = (/) ) )
235 234 adantr 
 |-  ( ( ph /\ a e. A ) -> ( ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) e. { (/) } <-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) = (/) ) )
236 230 235 mpbird 
 |-  ( ( ph /\ a e. A ) -> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) e. { (/) } )
237 236 3 fmptd 
 |-  ( ph -> F : A --> { (/) } )
238 237 adantr 
 |-  ( ( ph /\ d e. B ) -> F : A --> { (/) } )
239 ffvelrn 
 |-  ( ( G : B --> A /\ (/) e. B ) -> ( G ` (/) ) e. A )
240 11 211 239 syl2anc 
 |-  ( ph -> ( G ` (/) ) e. A )
241 240 adantr 
 |-  ( ( ph /\ d e. B ) -> ( G ` (/) ) e. A )
242 fvconst 
 |-  ( ( F : A --> { (/) } /\ ( G ` (/) ) e. A ) -> ( F ` ( G ` (/) ) ) = (/) )
243 238 241 242 syl2anc 
 |-  ( ( ph /\ d e. B ) -> ( F ` ( G ` (/) ) ) = (/) )
244 225 243 eqtrd 
 |-  ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = (/) )
245 223 eqcomd 
 |-  ( ( ph /\ d e. B ) -> (/) = d )
246 244 245 eqtrd 
 |-  ( ( ph /\ d e. B ) -> ( F ` ( G ` d ) ) = d )
247 246 ralrimiva 
 |-  ( ph -> A. d e. B ( F ` ( G ` d ) ) = d )
248 10 11 154 247 2fvidf1od 
 |-  ( ph -> F : A -1-1-onto-> B )