Theorem sticksstones15

Description: Sticks and stones with almost collapsed definitions for positive integers. (Contributed by metakunt, 7-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones15.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sticksstones15.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
	sticksstones15.3	⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
Assertion	sticksstones15	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + 𝐾 ) C 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		sticksstones15.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		sticksstones15.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3		sticksstones15.3	⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
4		eqid	⊢ ( 𝑣 ∈ 𝐴 ↦ ( 𝑧 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑧 + Σ 𝑡 ∈ ( 1 ... 𝑧 ) ( 𝑣 ‘ 𝑡 ) ) ) ) = ( 𝑣 ∈ 𝐴 ↦ ( 𝑧 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑧 + Σ 𝑡 ∈ ( 1 ... 𝑧 ) ( 𝑣 ‘ 𝑡 ) ) ) )
5		eqid	⊢ ( 𝑢 ∈ { 𝑙 ∣ ( 𝑙 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑙 ‘ 𝑥 ) < ( 𝑙 ‘ 𝑦 ) ) ) } ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑤 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑤 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑢 ‘ 𝐾 ) ) , if ( 𝑤 = 1 , ( ( 𝑢 ‘ 1 ) − 1 ) , ( ( ( 𝑢 ‘ 𝑤 ) − ( 𝑢 ‘ ( 𝑤 − 1 ) ) ) − 1 ) ) ) ) ) ) = ( 𝑢 ∈ { 𝑙 ∣ ( 𝑙 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑙 ‘ 𝑥 ) < ( 𝑙 ‘ 𝑦 ) ) ) } ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑤 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑤 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑢 ‘ 𝐾 ) ) , if ( 𝑤 = 1 , ( ( 𝑢 ‘ 1 ) − 1 ) , ( ( ( 𝑢 ‘ 𝑤 ) − ( 𝑢 ‘ ( 𝑤 − 1 ) ) ) − 1 ) ) ) ) ) )
6		feq1	⊢ ( 𝑙 = 𝑓 → ( 𝑙 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
7		fveq1	⊢ ( 𝑙 = 𝑓 → ( 𝑙 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑥 ) )
8		fveq1	⊢ ( 𝑙 = 𝑓 → ( 𝑙 ‘ 𝑦 ) = ( 𝑓 ‘ 𝑦 ) )
9	7 8	breq12d	⊢ ( 𝑙 = 𝑓 → ( ( 𝑙 ‘ 𝑥 ) < ( 𝑙 ‘ 𝑦 ) ↔ ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) )
10	9	imbi2d	⊢ ( 𝑙 = 𝑓 → ( ( 𝑥 < 𝑦 → ( 𝑙 ‘ 𝑥 ) < ( 𝑙 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) )
11	10	2ralbidv	⊢ ( 𝑙 = 𝑓 → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑙 ‘ 𝑥 ) < ( 𝑙 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) )
12	6 11	anbi12d	⊢ ( 𝑙 = 𝑓 → ( ( 𝑙 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑙 ‘ 𝑥 ) < ( 𝑙 ‘ 𝑦 ) ) ) ↔ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ) )
13	12	cbvabv	⊢ { 𝑙 ∣ ( 𝑙 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑙 ‘ 𝑥 ) < ( 𝑙 ‘ 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
14	1 2 4 5 3 13	sticksstones14	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + 𝐾 ) C 𝐾 ) )