Theorem sticksstones21

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

	Ref	Expression
Hypotheses	sticksstones21.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sticksstones21.2	⊢ ( 𝜑 → 𝑆 ∈ Fin )
	sticksstones21.3	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
	sticksstones21.4	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) = 𝑁 ) }
Assertion	sticksstones21	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + ( ( ♯ ‘ 𝑆 ) − 1 ) ) C ( ( ♯ ‘ 𝑆 ) − 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sticksstones21.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		sticksstones21.2	⊢ ( 𝜑 → 𝑆 ∈ Fin )
3		sticksstones21.3	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
4		sticksstones21.4	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) = 𝑁 ) }
5		hashnncl	⊢ ( 𝑆 ∈ Fin → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ↔ 𝑆 ≠ ∅ ) )
6	2 5	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ↔ 𝑆 ≠ ∅ ) )
7	3 6	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℕ )
8		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑔 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑘 ) )
9	8	cbvsumv	⊢ Σ 𝑗 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑗 ) = Σ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑘 )
10	9	eqeq1i	⊢ ( Σ 𝑗 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ↔ Σ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑘 ) = 𝑁 )
11	10	anbi2i	⊢ ( ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑆 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) ↔ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑆 ) ) ⟶ ℕ0 ∧ Σ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑘 ) = 𝑁 ) )
12	11	abbii	⊢ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑆 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑆 ) ) ⟶ ℕ0 ∧ Σ 𝑘 ∈ ( 1 ... ( ♯ ‘ 𝑆 ) ) ( 𝑔 ‘ 𝑘 ) = 𝑁 ) }
13		fveq2	⊢ ( 𝑖 = 𝑘 → ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑘 ) )
14	13	cbvsumv	⊢ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) = Σ 𝑘 ∈ 𝑆 ( 𝑓 ‘ 𝑘 )
15	14	eqeq1i	⊢ ( Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑘 ∈ 𝑆 ( 𝑓 ‘ 𝑘 ) = 𝑁 )
16	15	anbi2i	⊢ ( ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑆 ( 𝑓 ‘ 𝑘 ) = 𝑁 ) )
17	16	abbii	⊢ { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) = 𝑁 ) } = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑆 ( 𝑓 ‘ 𝑘 ) = 𝑁 ) }
18	4 17	eqtri	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑘 ∈ 𝑆 ( 𝑓 ‘ 𝑘 ) = 𝑁 ) }
19		eqidd	⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ 𝑆 ) )
20	1 2 7 12 18 19	sticksstones20	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + ( ( ♯ ‘ 𝑆 ) − 1 ) ) C ( ( ♯ ‘ 𝑆 ) − 1 ) ) )