Theorem sticksstones15

Description: Sticks and stones with almost collapsed definitions for positive integers. (Contributed by metakunt, 7-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones15.1	|- ( ph -> N e. NN0 )
	sticksstones15.2	|- ( ph -> K e. NN0 )
	sticksstones15.3	|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
Assertion	sticksstones15	|- ( ph -> ( # ` A ) = ( ( N + K ) _C K ) )

Proof

Step	Hyp	Ref	Expression
1		sticksstones15.1	|- ( ph -> N e. NN0 )
2		sticksstones15.2	|- ( ph -> K e. NN0 )
3		sticksstones15.3	|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
4		eqid	|- ( v e. A |-> ( z e. ( 1 ... K ) |-> ( z + sum_ t e. ( 1 ... z ) ( v ` t ) ) ) ) = ( v e. A |-> ( z e. ( 1 ... K ) |-> ( z + sum_ t e. ( 1 ... z ) ( v ` t ) ) ) )
5		eqid	|- ( u e. { l | ( l : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( l ` x ) < ( l ` y ) ) ) } |-> if ( K = 0 , { <. 1 , N >. } , ( w e. ( 1 ... ( K + 1 ) ) |-> if ( w = ( K + 1 ) , ( ( N + K ) - ( u ` K ) ) , if ( w = 1 , ( ( u ` 1 ) - 1 ) , ( ( ( u ` w ) - ( u ` ( w - 1 ) ) ) - 1 ) ) ) ) ) ) = ( u e. { l | ( l : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( l ` x ) < ( l ` y ) ) ) } |-> if ( K = 0 , { <. 1 , N >. } , ( w e. ( 1 ... ( K + 1 ) ) |-> if ( w = ( K + 1 ) , ( ( N + K ) - ( u ` K ) ) , if ( w = 1 , ( ( u ` 1 ) - 1 ) , ( ( ( u ` w ) - ( u ` ( w - 1 ) ) ) - 1 ) ) ) ) ) )
6		feq1	|- ( l = f -> ( l : ( 1 ... K ) --> ( 1 ... ( N + K ) ) <-> f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) ) )
7		fveq1	|- ( l = f -> ( l ` x ) = ( f ` x ) )
8		fveq1	|- ( l = f -> ( l ` y ) = ( f ` y ) )
9	7 8	breq12d	|- ( l = f -> ( ( l ` x ) < ( l ` y ) <-> ( f ` x ) < ( f ` y ) ) )
10	9	imbi2d	|- ( l = f -> ( ( x < y -> ( l ` x ) < ( l ` y ) ) <-> ( x < y -> ( f ` x ) < ( f ` y ) ) ) )
11	10	2ralbidv	|- ( l = f -> ( A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( l ` x ) < ( l ` y ) ) <-> A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) )
12	6 11	anbi12d	|- ( l = f -> ( ( l : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( l ` x ) < ( l ` y ) ) ) <-> ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) ) )
13	12	cbvabv	|- { l | ( l : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( l ` x ) < ( l ` y ) ) ) } = { f | ( f : ( 1 ... K ) --> ( 1 ... ( N + K ) ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
14	1 2 4 5 3 13	sticksstones14	|- ( ph -> ( # ` A ) = ( ( N + K ) _C K ) )