Metamath Proof Explorer

Theorem sticksstones14

Description: Sticks and stones with definitions as hypotheses. (Contributed by metakunt, 7-Oct-2024)

Ref Expression
Hypotheses sticksstones14.1 
|- ( ph -> N e. NN0 )
sticksstones14.2 
|- ( ph -> K e. NN0 )
sticksstones14.3 
|- F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
sticksstones14.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 ) ) ) ) ) )
sticksstones14.5 
|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
sticksstones14.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 sticksstones14 
|- ( ph -> ( # ` A ) = ( ( N + K ) _C K ) )

Proof

Step Hyp Ref Expression
1 sticksstones14.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones14.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones14.3 
 |-  F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
4 sticksstones14.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 sticksstones14.5 
 |-  A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
6 sticksstones14.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 5 a1i 
 |-  ( ph -> A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } )
8 simpl 
 |-  ( ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) -> g : ( 1 ... ( K + 1 ) ) --> NN0 )
9 8 a1i 
 |-  ( ph -> ( ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) -> g : ( 1 ... ( K + 1 ) ) --> NN0 ) )
10 9 ss2abdv 
 |-  ( ph -> { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } C_ { g | g : ( 1 ... ( K + 1 ) ) --> NN0 } )
11 fzfid 
 |-  ( ph -> ( 1 ... ( K + 1 ) ) e. Fin )
12 nn0ex 
 |-  NN0 e. _V
13 12 a1i 
 |-  ( ph -> NN0 e. _V )
14 mapex 
 |-  ( ( ( 1 ... ( K + 1 ) ) e. Fin /\ NN0 e. _V ) -> { g | g : ( 1 ... ( K + 1 ) ) --> NN0 } e. _V )
15 11 13 14 syl2anc 
 |-  ( ph -> { g | g : ( 1 ... ( K + 1 ) ) --> NN0 } e. _V )
16 ssexg 
 |-  ( ( { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } C_ { g | g : ( 1 ... ( K + 1 ) ) --> NN0 } /\ { g | g : ( 1 ... ( K + 1 ) ) --> NN0 } e. _V ) -> { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } e. _V )
17 10 15 16 syl2anc 
 |-  ( ph -> { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) } e. _V )
18 7 17 eqeltrd 
 |-  ( ph -> A e. _V )
19 1 2 3 4 5 6 sticksstones13 
 |-  ( ph -> F : A -1-1-onto-> B )
20 18 19 hasheqf1od 
 |-  ( ph -> ( # ` A ) = ( # ` B ) )
21 1 2 nn0addcld 
 |-  ( ph -> ( N + K ) e. NN0 )
22 21 2 6 sticksstones5 
 |-  ( ph -> ( # ` B ) = ( ( N + K ) _C K ) )
23 20 22 eqtrd 
 |-  ( ph -> ( # ` A ) = ( ( N + K ) _C K ) )