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	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sticksstones13.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	sticksstones13.3	$$⊢F=\left(a\in A⟼\left(j\in \left(1\dots K\right)⟼j+\sum _{l=1}^{j}a\left(l\right)\right)\right)$$
	sticksstones13.4	$$⊢G=\left(b\in B⟼if\left(K=0,\left\{⟨1,N⟩\right\},\left(k\in \left(1\dots K+1\right)⟼if\left(k=K+1,N+K-b\left(K\right),if\left(k=1,b\left(1\right)-1,b\left(k\right)-b\left(k-1\right)-1\right)\right)\right)\right)\right)$$
	sticksstones13.5	$$⊢A=\left\{g|\left(g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K+1}g\left(i\right)=N\right)\right\}$$
	sticksstones13.6	$$⊢B=\left\{f|\left(f:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to f\left(x\right)<f\left(y\right)\right)\right)\right\}$$
Assertion	sticksstones13	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		sticksstones13.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		sticksstones13.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
3		sticksstones13.3	$$⊢F=\left(a\in A⟼\left(j\in \left(1\dots K\right)⟼j+\sum _{l=1}^{j}a\left(l\right)\right)\right)$$
4		sticksstones13.4	$$⊢G=\left(b\in B⟼if\left(K=0,\left\{⟨1,N⟩\right\},\left(k\in \left(1\dots K+1\right)⟼if\left(k=K+1,N+K-b\left(K\right),if\left(k=1,b\left(1\right)-1,b\left(k\right)-b\left(k-1\right)-1\right)\right)\right)\right)\right)$$
5		sticksstones13.5	$$⊢A=\left\{g|\left(g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K+1}g\left(i\right)=N\right)\right\}$$
6		sticksstones13.6	$$⊢B=\left\{f|\left(f:\left(1\dots K\right)⟶\left(1\dots N+K\right)\wedge \forall x\in \left(1\dots K\right)\forall y\in \left(1\dots K\right)\left(x<y\to f\left(x\right)<f\left(y\right)\right)\right)\right\}$$
7	1	adantr	$$⊢\left(\phi \wedge K=0\right)\to N\in {\mathbb{N}}_0$$
8		simpr	$$⊢\left(\phi \wedge K=0\right)\to K=0$$
9	7 8 3 4 5 6	sticksstones11	$$⊢\left(\phi \wedge K=0\right)\to F:A\underset{1-1\; onto}{⟶}B$$
10	1	adantr	$$⊢\left(\phi \wedge K\in \mathbb{N}\right)\to N\in {\mathbb{N}}_0$$
11		simpr	$$⊢\left(\phi \wedge K\in \mathbb{N}\right)\to K\in \mathbb{N}$$
12	10 11 3 4 5 6	sticksstones12	$$⊢\left(\phi \wedge K\in \mathbb{N}\right)\to F:A\underset{1-1\; onto}{⟶}B$$
13		elnn0	$$⊢K\in {\mathbb{N}}_0\leftrightarrow \left(K\in \mathbb{N}\vee K=0\right)$$
14	13	biimpi	$$⊢K\in {\mathbb{N}}_0\to \left(K\in \mathbb{N}\vee K=0\right)$$
15	14	orcomd	$$⊢K\in {\mathbb{N}}_0\to \left(K=0\vee K\in \mathbb{N}\right)$$
16	2 15	syl	$$⊢\phi \to \left(K=0\vee K\in \mathbb{N}\right)$$
17	9 12 16	mpjaodan	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$