Theorem sticksstones14

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

	Ref	Expression
Hypotheses	sticksstones14.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sticksstones14.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
	sticksstones14.3	⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
	sticksstones14.4	⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
	sticksstones14.5	⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
	sticksstones14.6	⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
Assertion	sticksstones14	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + 𝐾 ) C 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		sticksstones14.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		sticksstones14.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3		sticksstones14.3	⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
4		sticksstones14.4	⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
5		sticksstones14.5	⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
6		sticksstones14.6	⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
7	5	a1i	⊢ ( 𝜑 → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
8		simpl	⊢ ( ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) → 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
9	8	a1i	⊢ ( 𝜑 → ( ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) → 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ) )
10	9	ss2abdv	⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ⊆ { 𝑔 ∣ 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 } )
11		fzfid	⊢ ( 𝜑 → ( 1 ... ( 𝐾 + 1 ) ) ∈ Fin )
12		nn0ex	⊢ ℕ0 ∈ V
13	12	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
14		mapex	⊢ ( ( ( 1 ... ( 𝐾 + 1 ) ) ∈ Fin ∧ ℕ0 ∈ V ) → { 𝑔 ∣ 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 } ∈ V )
15	11 13 14	syl2anc	⊢ ( 𝜑 → { 𝑔 ∣ 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 } ∈ V )
16		ssexg	⊢ ( ( { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ⊆ { 𝑔 ∣ 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 } ∧ { 𝑔 ∣ 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 } ∈ V ) → { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ∈ V )
17	10 15 16	syl2anc	⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ∈ V )
18	7 17	eqeltrd	⊢ ( 𝜑 → 𝐴 ∈ V )
19	1 2 3 4 5 6	sticksstones13	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
20	18 19	hasheqf1od	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐵 ) )
21	1 2	nn0addcld	⊢ ( 𝜑 → ( 𝑁 + 𝐾 ) ∈ ℕ0 )
22	21 2 6	sticksstones5	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) = ( ( 𝑁 + 𝐾 ) C 𝐾 ) )
23	20 22	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + 𝐾 ) C 𝐾 ) )