Metamath Proof Explorer

Theorem sticksstones20

Description: Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakung, 24-Oct-2024)

Ref Expression
Hypotheses sticksstones20.1 
|- ( ph -> N e. NN0 )
sticksstones20.2 
|- ( ph -> S e. Fin )
sticksstones20.3 
|- ( ph -> K e. NN )
sticksstones20.4 
|- A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
sticksstones20.5 
|- B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
sticksstones20.6 
|- ( ph -> ( # ` S ) = K )
Assertion sticksstones20 
|- ( ph -> ( # ` B ) = ( ( N + ( K - 1 ) ) _C ( K - 1 ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones20.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones20.2 
 |-  ( ph -> S e. Fin )
3 sticksstones20.3 
 |-  ( ph -> K e. NN )
4 sticksstones20.4 
 |-  A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) }
5 sticksstones20.5 
 |-  B = { h | ( h : S --> NN0 /\ sum_ i e. S ( h ` i ) = N ) }
6 sticksstones20.6 
 |-  ( ph -> ( # ` S ) = K )
7 isfinite4 
 |-  ( S e. Fin <-> ( 1 ... ( # ` S ) ) ~~ S )
8 bren 
 |-  ( ( 1 ... ( # ` S ) ) ~~ S <-> E. p p : ( 1 ... ( # ` S ) ) -1-1-onto-> S )
9 7 8 sylbb 
 |-  ( S e. Fin -> E. p p : ( 1 ... ( # ` S ) ) -1-1-onto-> S )
10 2 9 syl 
 |-  ( ph -> E. p p : ( 1 ... ( # ` S ) ) -1-1-onto-> S )
11 6 oveq2d 
 |-  ( ph -> ( 1 ... ( # ` S ) ) = ( 1 ... K ) )
12 11 f1oeq2d 
 |-  ( ph -> ( p : ( 1 ... ( # ` S ) ) -1-1-onto-> S <-> p : ( 1 ... K ) -1-1-onto-> S ) )
13 12 biimpd 
 |-  ( ph -> ( p : ( 1 ... ( # ` S ) ) -1-1-onto-> S -> p : ( 1 ... K ) -1-1-onto-> S ) )
14 13 eximdv 
 |-  ( ph -> ( E. p p : ( 1 ... ( # ` S ) ) -1-1-onto-> S -> E. p p : ( 1 ... K ) -1-1-onto-> S ) )
15 10 14 mpd 
 |-  ( ph -> E. p p : ( 1 ... K ) -1-1-onto-> S )
16 4 a1i 
 |-  ( ph -> A = { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } )
17 fzfid 
 |-  ( ph -> ( 1 ... K ) e. Fin )
18 nn0ex 
 |-  NN0 e. _V
19 18 a1i 
 |-  ( ph -> NN0 e. _V )
20 mapex 
 |-  ( ( ( 1 ... K ) e. Fin /\ NN0 e. _V ) -> { g | g : ( 1 ... K ) --> NN0 } e. _V )
21 17 19 20 syl2anc 
 |-  ( ph -> { g | g : ( 1 ... K ) --> NN0 } e. _V )
22 simprl 
 |-  ( ( ph /\ ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) ) -> g : ( 1 ... K ) --> NN0 )
23 22 ex 
 |-  ( ph -> ( ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) -> g : ( 1 ... K ) --> NN0 ) )
24 23 ss2abdv 
 |-  ( ph -> { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } C_ { g | g : ( 1 ... K ) --> NN0 } )
25 21 24 ssexd 
 |-  ( ph -> { g | ( g : ( 1 ... K ) --> NN0 /\ sum_ i e. ( 1 ... K ) ( g ` i ) = N ) } e. _V )
26 16 25 eqeltrd 
 |-  ( ph -> A e. _V )
27 26 adantr 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> A e. _V )
28 27 mptexd 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> ( a e. A |-> ( x e. S |-> ( a ` ( `' p ` x ) ) ) ) e. _V )
29 1 adantr 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> N e. NN0 )
30 3 nnnn0d 
 |-  ( ph -> K e. NN0 )
31 30 adantr 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> K e. NN0 )
32 simpr 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> p : ( 1 ... K ) -1-1-onto-> S )
33 eqid 
 |-  ( a e. A |-> ( x e. S |-> ( a ` ( `' p ` x ) ) ) ) = ( a e. A |-> ( x e. S |-> ( a ` ( `' p ` x ) ) ) )
34 eqid 
 |-  ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( p ` y ) ) ) ) = ( b e. B |-> ( y e. ( 1 ... K ) |-> ( b ` ( p ` y ) ) ) )
35 29 31 4 5 32 33 34 sticksstones19 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> ( a e. A |-> ( x e. S |-> ( a ` ( `' p ` x ) ) ) ) : A -1-1-onto-> B )
36 f1oeq1 
 |-  ( q = ( a e. A |-> ( x e. S |-> ( a ` ( `' p ` x ) ) ) ) -> ( q : A -1-1-onto-> B <-> ( a e. A |-> ( x e. S |-> ( a ` ( `' p ` x ) ) ) ) : A -1-1-onto-> B ) )
37 28 35 36 spcedv 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> E. q q : A -1-1-onto-> B )
38 bren 
 |-  ( A ~~ B <-> E. q q : A -1-1-onto-> B )
39 37 38 sylibr 
 |-  ( ( ph /\ p : ( 1 ... K ) -1-1-onto-> S ) -> A ~~ B )
40 15 39 exlimddv 
 |-  ( ph -> A ~~ B )
41 hasheni 
 |-  ( A ~~ B -> ( # ` A ) = ( # ` B ) )
42 40 41 syl 
 |-  ( ph -> ( # ` A ) = ( # ` B ) )
43 42 eqcomd 
 |-  ( ph -> ( # ` B ) = ( # ` A ) )
44 1 3 4 sticksstones16 
 |-  ( ph -> ( # ` A ) = ( ( N + ( K - 1 ) ) _C ( K - 1 ) ) )
45 43 44 eqtrd 
 |-  ( ph -> ( # ` B ) = ( ( N + ( K - 1 ) ) _C ( K - 1 ) ) )