Theorem sticksstones13

Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		sticksstones13.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		sticksstones13.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3		sticksstones13.3	⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
4		sticksstones13.4	⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
5		sticksstones13.5	⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
6		sticksstones13.6	⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
7	1	adantr	⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → 𝑁 ∈ ℕ0 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → 𝐾 = 0 )
9	7 8 3 4 5 6	sticksstones11	⊢ ( ( 𝜑 ∧ 𝐾 = 0 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
10	1	adantr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
11		simpr	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → 𝐾 ∈ ℕ )
12	10 11 3 4 5 6	sticksstones12	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℕ ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
13		elnn0	⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
14	13	biimpi	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
15	14	orcomd	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 = 0 ∨ 𝐾 ∈ ℕ ) )
16	2 15	syl	⊢ ( 𝜑 → ( 𝐾 = 0 ∨ 𝐾 ∈ ℕ ) )
17	9 12 16	mpjaodan	⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )