Theorem sticksstones13

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

Proof

Step	Hyp	Ref	Expression
1		sticksstones13.1	|- ( ph -> N e. NN0 )
2		sticksstones13.2	|- ( ph -> K e. NN0 )
3		sticksstones13.3	|- F = ( a e. A |-> ( j e. ( 1 ... K ) |-> ( j + sum_ l e. ( 1 ... j ) ( a ` l ) ) ) )
4		sticksstones13.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		sticksstones13.5	|- A = { g | ( g : ( 1 ... ( K + 1 ) ) --> NN0 /\ sum_ i e. ( 1 ... ( K + 1 ) ) ( g ` i ) = N ) }
6		sticksstones13.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	1	adantr	|- ( ( ph /\ K = 0 ) -> N e. NN0 )
8		simpr	|- ( ( ph /\ K = 0 ) -> K = 0 )
9	7 8 3 4 5 6	sticksstones11	|- ( ( ph /\ K = 0 ) -> F : A -1-1-onto-> B )
10	1	adantr	|- ( ( ph /\ K e. NN ) -> N e. NN0 )
11		simpr	|- ( ( ph /\ K e. NN ) -> K e. NN )
12	10 11 3 4 5 6	sticksstones12	|- ( ( ph /\ K e. NN ) -> F : A -1-1-onto-> B )
13		elnn0	|- ( K e. NN0 <-> ( K e. NN \/ K = 0 ) )
14	13	biimpi	|- ( K e. NN0 -> ( K e. NN \/ K = 0 ) )
15	14	orcomd	|- ( K e. NN0 -> ( K = 0 \/ K e. NN ) )
16	2 15	syl	|- ( ph -> ( K = 0 \/ K e. NN ) )
17	9 12 16	mpjaodan	|- ( ph -> F : A -1-1-onto-> B )