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	$⊢ φ \to N \in ℕ_{0}$
	sticksstones5.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones5.3	$⊢ A = \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
Assertion	sticksstones5	$⊢ φ \to \|A\| = (\binom{N}{K})$

Step	Hyp	Ref	Expression
1		sticksstones5.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones5.2	$⊢ φ \to K \in ℕ_{0}$
3		sticksstones5.3	$⊢ A = \{f \| (f : (1 \dots K) ⟶ (1 \dots N) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
4		eqid	$⊢ \{s \in 𝒫 (1 \dots N) \| \|s\| = K\} = \{s \in 𝒫 (1 \dots N) \| \|s\| = K\}$
5	1 2 4 3	sticksstones4	$⊢ φ \to A \approx \{s \in 𝒫 (1 \dots N) \| \|s\| = K\}$
6		hasheni	$⊢ A \approx \{s \in 𝒫 (1 \dots N) \| \|s\| = K\} \to \|A\| = \|\{s \in 𝒫 (1 \dots N) \| \|s\| = K\}\|$
7	5 6	syl	$⊢ φ \to \|A\| = \|\{s \in 𝒫 (1 \dots N) \| \|s\| = K\}\|$
8		fzfid	$⊢ φ \to (1 \dots N) \in Fin$
9	2	nn0zd	$⊢ φ \to K \in ℤ$
10		hashbc	$⊢ ((1 \dots N) \in Fin \land K \in ℤ) \to (\binom{\|(1 \dots N)\|}{K}) = \|\{s \in 𝒫 (1 \dots N) \| \|s\| = K\}\|$
11	8 9 10	syl2anc	$⊢ φ \to (\binom{\|(1 \dots N)\|}{K}) = \|\{s \in 𝒫 (1 \dots N) \| \|s\| = K\}\|$
12	11	eqcomd	$⊢ φ \to \|\{s \in 𝒫 (1 \dots N) \| \|s\| = K\}\| = (\binom{\|(1 \dots N)\|}{K})$
13		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
14	1 13	syl	$⊢ φ \to \|(1 \dots N)\| = N$
15	14	oveq1d	$⊢ φ \to (\binom{\|(1 \dots N)\|}{K}) = (\binom{N}{K})$
16	12 15	eqtrd	$⊢ φ \to \|\{s \in 𝒫 (1 \dots N) \| \|s\| = K\}\| = (\binom{N}{K})$
17	7 16	eqtrd	$⊢ φ \to \|A\| = (\binom{N}{K})$

Metamath Proof Explorer