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	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sticksstones5.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
	sticksstones5.3	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
Assertion	sticksstones5	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( 𝑁 C 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		sticksstones5.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		sticksstones5.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3		sticksstones5.3	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... 𝑁 ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
4		eqid	⊢ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } = { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 }
5	1 2 4 3	sticksstones4	⊢ ( 𝜑 → 𝐴 ≈ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } )
6		hasheni	⊢ ( 𝐴 ≈ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } ) )
7	5 6	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } ) )
8		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
9	2	nn0zd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
10		hashbc	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝐾 ∈ ℤ ) → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) C 𝐾 ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } ) )
11	8 9 10	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) C 𝐾 ) = ( ♯ ‘ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } ) )
12	11	eqcomd	⊢ ( 𝜑 → ( ♯ ‘ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } ) = ( ( ♯ ‘ ( 1 ... 𝑁 ) ) C 𝐾 ) )
13		hashfz1	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
14	1 13	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
15	14	oveq1d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 1 ... 𝑁 ) ) C 𝐾 ) = ( 𝑁 C 𝐾 ) )
16	12 15	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ { 𝑠 ∈ 𝒫 ( 1 ... 𝑁 ) ∣ ( ♯ ‘ 𝑠 ) = 𝐾 } ) = ( 𝑁 C 𝐾 ) )
17	7 16	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( 𝑁 C 𝐾 ) )