Theorem sticksstones14

Description: Sticks and stones with definitions as hypotheses. (Contributed by metakunt, 7-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones14.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sticksstones14.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
	sticksstones14.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)$$
	sticksstones14.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)$$
	sticksstones14.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\}$$
	sticksstones14.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	sticksstones14	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+K}{K}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sticksstones14.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		sticksstones14.2	$$⊢\phi \to K\in {\mathbb{N}}_0$$
3		sticksstones14.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		sticksstones14.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		sticksstones14.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		sticksstones14.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	5	a1i	$$⊢\phi \to 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\}$$
8		simpl	$$⊢\left(g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K+1}g\left(i\right)=N\right)\to g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0$$
9	8	a1i	$$⊢\phi \to \left(\left(g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K+1}g\left(i\right)=N\right)\to g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\right)$$
10	9	ss2abdv	$$⊢\phi \to \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\}\subseteq \left\{g|g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\right\}$$
11		fzfid	$$⊢\phi \to \left(1\dots K+1\right)\in \mathrm{Fin}$$
12		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
13	12	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
14		mapex	$$⊢\left(\left(1\dots K+1\right)\in \mathrm{Fin}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left\{g|g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\right\}\in \mathrm{V}$$
15	11 13 14	syl2anc	$$⊢\phi \to \left\{g|g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\right\}\in \mathrm{V}$$
16		ssexg	$$⊢\left(\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\}\subseteq \left\{g|g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\right\}\wedge \left\{g|g:\left(1\dots K+1\right)⟶{\mathbb{N}}_0\right\}\in \mathrm{V}\right)\to \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\}\in \mathrm{V}$$
17	10 15 16	syl2anc	$$⊢\phi \to \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\}\in \mathrm{V}$$
18	7 17	eqeltrd	$$⊢\phi \to A\in \mathrm{V}$$
19	1 2 3 4 5 6	sticksstones13	$$⊢\phi \to F:A\underset{1-1\; onto}{⟶}B$$
20	18 19	hasheqf1od	$$⊢\phi \to \left|A\right|=\left|B\right|$$
21	1 2	nn0addcld	$$⊢\phi \to N+K\in {\mathbb{N}}_0$$
22	21 2 6	sticksstones5	$$⊢\phi \to \left|B\right|=\left(\genfrac{}{}{0ex}{}{N+K}{K}\right)$$
23	20 22	eqtrd	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+K}{K}\right)$$