Theorem sticksstones5

Description: Count the number of strictly monotonely increasing functions on finite domains and codomains. (Contributed by metakunt, 28-Sep-2024)

	Ref	Expression
Hypotheses	sticksstones5.1	|- ( ph -> N e. NN0 )
	sticksstones5.2	|- ( ph -> K e. NN0 )
	sticksstones5.3	|- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
Assertion	sticksstones5	|- ( ph -> ( # ` A ) = ( N _C K ) )

Proof

Step	Hyp	Ref	Expression
1		sticksstones5.1	|- ( ph -> N e. NN0 )
2		sticksstones5.2	|- ( ph -> K e. NN0 )
3		sticksstones5.3	|- A = { f | ( f : ( 1 ... K ) --> ( 1 ... N ) /\ A. x e. ( 1 ... K ) A. y e. ( 1 ... K ) ( x < y -> ( f ` x ) < ( f ` y ) ) ) }
4		eqid	|- { s e. ~P ( 1 ... N ) | ( # ` s ) = K } = { s e. ~P ( 1 ... N ) | ( # ` s ) = K }
5	1 2 4 3	sticksstones4	|- ( ph -> A ~~ { s e. ~P ( 1 ... N ) | ( # ` s ) = K } )
6		hasheni	|- ( A ~~ { s e. ~P ( 1 ... N ) | ( # ` s ) = K } -> ( # ` A ) = ( # ` { s e. ~P ( 1 ... N ) | ( # ` s ) = K } ) )
7	5 6	syl	|- ( ph -> ( # ` A ) = ( # ` { s e. ~P ( 1 ... N ) | ( # ` s ) = K } ) )
8		fzfid	|- ( ph -> ( 1 ... N ) e. Fin )
9	2	nn0zd	|- ( ph -> K e. ZZ )
10		hashbc	|- ( ( ( 1 ... N ) e. Fin /\ K e. ZZ ) -> ( ( # ` ( 1 ... N ) ) _C K ) = ( # ` { s e. ~P ( 1 ... N ) | ( # ` s ) = K } ) )
11	8 9 10	syl2anc	|- ( ph -> ( ( # ` ( 1 ... N ) ) _C K ) = ( # ` { s e. ~P ( 1 ... N ) | ( # ` s ) = K } ) )
12	11	eqcomd	|- ( ph -> ( # ` { s e. ~P ( 1 ... N ) | ( # ` s ) = K } ) = ( ( # ` ( 1 ... N ) ) _C K ) )
13		hashfz1	|- ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
14	1 13	syl	|- ( ph -> ( # ` ( 1 ... N ) ) = N )
15	14	oveq1d	|- ( ph -> ( ( # ` ( 1 ... N ) ) _C K ) = ( N _C K ) )
16	12 15	eqtrd	|- ( ph -> ( # ` { s e. ~P ( 1 ... N ) | ( # ` s ) = K } ) = ( N _C K ) )
17	7 16	eqtrd	|- ( ph -> ( # ` A ) = ( N _C K ) )