Theorem sticksstones23

Description: Non-exhaustive sticks and stones. (Contributed by metakunt, 7-May-2025)

	Ref	Expression
Hypotheses	sticksstones23.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sticksstones23.2	$$⊢\phi \to S\in \mathrm{Fin}$$
	sticksstones23.3	$$⊢\phi \to S\ne \varnothing$$
	sticksstones23.4	$$⊢A=\left\{f\in \left({{\mathbb{N}}_0}^S\right)|\sum _{i\in S}f\left(i\right)\le N\right\}$$
Assertion	sticksstones23	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+\left|S\right|}{\left|S\right|}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sticksstones23.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		sticksstones23.2	$$⊢\phi \to S\in \mathrm{Fin}$$
3		sticksstones23.3	$$⊢\phi \to S\ne \varnothing$$
4		sticksstones23.4	$$⊢A=\left\{f\in \left({{\mathbb{N}}_0}^S\right)|\sum _{i\in S}f\left(i\right)\le N\right\}$$
5	4	a1i	$$⊢\phi \to A=\left\{f\in \left({{\mathbb{N}}_0}^S\right)|\sum _{i\in S}f\left(i\right)\le N\right\}$$
6		df-rab	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^S\right)|\sum _{i\in S}f\left(i\right)\le N\right\}=\left\{f|\left(f\in \left({{\mathbb{N}}_0}^S\right)\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}$$
7	6	a1i	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^S\right)|\sum _{i\in S}f\left(i\right)\le N\right\}=\left\{f|\left(f\in \left({{\mathbb{N}}_0}^S\right)\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}$$
8		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
10		elmapg	$$⊢\left({\mathbb{N}}_0\in \mathrm{V}\wedge S\in \mathrm{Fin}\right)\to \left(f\in \left({{\mathbb{N}}_0}^S\right)\leftrightarrow f:S⟶{\mathbb{N}}_0\right)$$
11	9 2 10	syl2anc	$$⊢\phi \to \left(f\in \left({{\mathbb{N}}_0}^S\right)\leftrightarrow f:S⟶{\mathbb{N}}_0\right)$$
12	11	anbi1d	$$⊢\phi \to \left(\left(f\in \left({{\mathbb{N}}_0}^S\right)\wedge \sum _{i\in S}f\left(i\right)\le N\right)\leftrightarrow \left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right)$$
13	12	abbidv	$$⊢\phi \to \left\{f|\left(f\in \left({{\mathbb{N}}_0}^S\right)\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}$$
14	7 13	eqtrd	$$⊢\phi \to \left\{f\in \left({{\mathbb{N}}_0}^S\right)|\sum _{i\in S}f\left(i\right)\le N\right\}=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}$$
15	5 14	eqtrd	$$⊢\phi \to A=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}$$
16	15	fveq2d	$$⊢\phi \to \left|A\right|=\left|\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}\right|$$
17		eqid	$$⊢\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}$$
18	1 2 3 17	sticksstones22	$$⊢\phi \to \left|\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)\le N\right)\right\}\right|=\left(\genfrac{}{}{0ex}{}{N+\left|S\right|}{\left|S\right|}\right)$$
19	16 18	eqtrd	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+\left|S\right|}{\left|S\right|}\right)$$