Theorem sticksstones20

Description: Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakung, 24-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones20.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sticksstones20.2	$$⊢\phi \to S\in \mathrm{Fin}$$
	sticksstones20.3	$$⊢\phi \to K\in \mathbb{N}$$
	sticksstones20.4	$$⊢A=\left\{g|\left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\right\}$$
	sticksstones20.5	$$⊢B=\left\{h|\left(h:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}h\left(i\right)=N\right)\right\}$$
	sticksstones20.6	$$⊢\phi \to \left|S\right|=K$$
Assertion	sticksstones20	$$⊢\phi \to \left|B\right|=\left(\genfrac{}{}{0ex}{}{N+K-1}{K-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sticksstones20.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		sticksstones20.2	$$⊢\phi \to S\in \mathrm{Fin}$$
3		sticksstones20.3	$$⊢\phi \to K\in \mathbb{N}$$
4		sticksstones20.4	$$⊢A=\left\{g|\left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\right\}$$
5		sticksstones20.5	$$⊢B=\left\{h|\left(h:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}h\left(i\right)=N\right)\right\}$$
6		sticksstones20.6	$$⊢\phi \to \left|S\right|=K$$
7		isfinite4	$$⊢S\in \mathrm{Fin}\leftrightarrow \left(1\dots \left|S\right|\right)\approx S$$
8		bren	$$⊢\left(1\dots \left|S\right|\right)\approx S\leftrightarrow \exists pp:\left(1\dots \left|S\right|\right)\underset{1-1\; onto}{⟶}S$$
9	7 8	sylbb	$$⊢S\in \mathrm{Fin}\to \exists pp:\left(1\dots \left|S\right|\right)\underset{1-1\; onto}{⟶}S$$
10	2 9	syl	$$⊢\phi \to \exists pp:\left(1\dots \left|S\right|\right)\underset{1-1\; onto}{⟶}S$$
11	6	oveq2d	$$⊢\phi \to \left(1\dots \left|S\right|\right)=\left(1\dots K\right)$$
12	11	f1oeq2d	$$⊢\phi \to \left(p:\left(1\dots \left|S\right|\right)\underset{1-1\; onto}{⟶}S\leftrightarrow p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)$$
13	12	biimpd	$$⊢\phi \to \left(p:\left(1\dots \left|S\right|\right)\underset{1-1\; onto}{⟶}S\to p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)$$
14	13	eximdv	$$⊢\phi \to \left(\exists pp:\left(1\dots \left|S\right|\right)\underset{1-1\; onto}{⟶}S\to \exists pp:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)$$
15	10 14	mpd	$$⊢\phi \to \exists pp:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S$$
16	4	a1i	$$⊢\phi \to A=\left\{g|\left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\right\}$$
17		fzfid	$$⊢\phi \to \left(1\dots K\right)\in \mathrm{Fin}$$
18		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
19	18	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
20		mapex	$$⊢\left(\left(1\dots K\right)\in \mathrm{Fin}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left\{g|g:\left(1\dots K\right)⟶{\mathbb{N}}_0\right\}\in \mathrm{V}$$
21	17 19 20	syl2anc	$$⊢\phi \to \left\{g|g:\left(1\dots K\right)⟶{\mathbb{N}}_0\right\}\in \mathrm{V}$$
22		simprl	$$⊢\left(\phi \wedge \left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\right)\to g:\left(1\dots K\right)⟶{\mathbb{N}}_0$$
23	22	ex	$$⊢\phi \to \left(\left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\to g:\left(1\dots K\right)⟶{\mathbb{N}}_0\right)$$
24	23	ss2abdv	$$⊢\phi \to \left\{g|\left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\right\}\subseteq \left\{g|g:\left(1\dots K\right)⟶{\mathbb{N}}_0\right\}$$
25	21 24	ssexd	$$⊢\phi \to \left\{g|\left(g:\left(1\dots K\right)⟶{\mathbb{N}}_0\wedge \sum _{i=1}^{K}g\left(i\right)=N\right)\right\}\in \mathrm{V}$$
26	16 25	eqeltrd	$$⊢\phi \to A\in \mathrm{V}$$
27	26	adantr	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to A\in \mathrm{V}$$
28	27	mptexd	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to \left(a\in A⟼\left(x\in S⟼a\left(p^{-1}\left(x\right)\right)\right)\right)\in \mathrm{V}$$
29	1	adantr	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to N\in {\mathbb{N}}_0$$
30	3	nnnn0d	$$⊢\phi \to K\in {\mathbb{N}}_0$$
31	30	adantr	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to K\in {\mathbb{N}}_0$$
32		simpr	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S$$
33		eqid	$$⊢\left(a\in A⟼\left(x\in S⟼a\left(p^{-1}\left(x\right)\right)\right)\right)=\left(a\in A⟼\left(x\in S⟼a\left(p^{-1}\left(x\right)\right)\right)\right)$$
34		eqid	$$⊢\left(b\in B⟼\left(y\in \left(1\dots K\right)⟼b\left(p\left(y\right)\right)\right)\right)=\left(b\in B⟼\left(y\in \left(1\dots K\right)⟼b\left(p\left(y\right)\right)\right)\right)$$
35	29 31 4 5 32 33 34	sticksstones19	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to \left(a\in A⟼\left(x\in S⟼a\left(p^{-1}\left(x\right)\right)\right)\right):A\underset{1-1\; onto}{⟶}B$$
36		f1oeq1	$$⊢q=\left(a\in A⟼\left(x\in S⟼a\left(p^{-1}\left(x\right)\right)\right)\right)\to \left(q:A\underset{1-1\; onto}{⟶}B\leftrightarrow \left(a\in A⟼\left(x\in S⟼a\left(p^{-1}\left(x\right)\right)\right)\right):A\underset{1-1\; onto}{⟶}B\right)$$
37	28 35 36	spcedv	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to \exists qq:A\underset{1-1\; onto}{⟶}B$$
38		bren	$$⊢A\approx B\leftrightarrow \exists qq:A\underset{1-1\; onto}{⟶}B$$
39	37 38	sylibr	$$⊢\left(\phi \wedge p:\left(1\dots K\right)\underset{1-1\; onto}{⟶}S\right)\to A\approx B$$
40	15 39	exlimddv	$$⊢\phi \to A\approx B$$
41		hasheni	$$⊢A\approx B\to \left|A\right|=\left|B\right|$$
42	40 41	syl	$$⊢\phi \to \left|A\right|=\left|B\right|$$
43	42	eqcomd	$$⊢\phi \to \left|B\right|=\left|A\right|$$
44	1 3 4	sticksstones16	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+K-1}{K-1}\right)$$
45	43 44	eqtrd	$$⊢\phi \to \left|B\right|=\left(\genfrac{}{}{0ex}{}{N+K-1}{K-1}\right)$$