Theorem sticksstones23

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

	Ref	Expression
Hypotheses	sticksstones23.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sticksstones23.2	⊢ ( 𝜑 → 𝑆 ∈ Fin )
	sticksstones23.3	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
	sticksstones23.4	⊢ 𝐴 = { 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∣ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 }
Assertion	sticksstones23	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + ( ♯ ‘ 𝑆 ) ) C ( ♯ ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sticksstones23.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		sticksstones23.2	⊢ ( 𝜑 → 𝑆 ∈ Fin )
3		sticksstones23.3	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
4		sticksstones23.4	⊢ 𝐴 = { 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∣ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 }
5	4	a1i	⊢ ( 𝜑 → 𝐴 = { 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∣ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 } )
6		df-rab	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∣ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 } = { 𝑓 ∣ ( 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) }
7	6	a1i	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∣ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 } = { 𝑓 ∣ ( 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } )
8		nn0ex	⊢ ℕ0 ∈ V
9	8	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
10		elmapg	⊢ ( ( ℕ0 ∈ V ∧ 𝑆 ∈ Fin ) → ( 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ↔ 𝑓 : 𝑆 ⟶ ℕ0 ) )
11	9 2 10	syl2anc	⊢ ( 𝜑 → ( 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ↔ 𝑓 : 𝑆 ⟶ ℕ0 ) )
12	11	anbi1d	⊢ ( 𝜑 → ( ( 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) ↔ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) ) )
13	12	abbidv	⊢ ( 𝜑 → { 𝑓 ∣ ( 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } )
14	7 13	eqtrd	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ0 ↑m 𝑆 ) ∣ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 } = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } )
15	5 14	eqtrd	⊢ ( 𝜑 → 𝐴 = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } )
16	15	fveq2d	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } ) )
17		eqid	⊢ { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) }
18	1 2 3 17	sticksstones22	⊢ ( 𝜑 → ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) } ) = ( ( 𝑁 + ( ♯ ‘ 𝑆 ) ) C ( ♯ ‘ 𝑆 ) ) )
19	16 18	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + ( ♯ ‘ 𝑆 ) ) C ( ♯ ‘ 𝑆 ) ) )