Metamath Proof Explorer

Theorem sticksstones9

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

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

Proof

Step Hyp Ref Expression
1 sticksstones9.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones9.2 ⊢ ( 𝜑 → 𝐾 = 0 )
3 sticksstones9.3 ⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) )
4 sticksstones9.4 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
5 sticksstones9.5 ⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
6 2 iftrued ⊢ ( 𝜑 → if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) = { ⟨ 1 , 𝑁 ⟩ } )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) = { ⟨ 1 , 𝑁 ⟩ } )
8 eqid ⊢ { ⟨ 1 , 𝑁 ⟩ } = { ⟨ 1 , 𝑁 ⟩ }
9 1nn ⊢ 1 ∈ ℕ
10 9 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
11 fsng ⊢ ( ( 1 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ { 𝑁 } ↔ { ⟨ 1 , 𝑁 ⟩ } = { ⟨ 1 , 𝑁 ⟩ } ) )
12 10 1 11 syl2anc ⊢ ( 𝜑 → ( { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ { 𝑁 } ↔ { ⟨ 1 , 𝑁 ⟩ } = { ⟨ 1 , 𝑁 ⟩ } ) )
13 8 12 mpbiri ⊢ ( 𝜑 → { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ { 𝑁 } )
14 1 snssd ⊢ ( 𝜑 → { 𝑁 } ⊆ ℕ0 )
15 13 14 jca ⊢ ( 𝜑 → ( { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ { 𝑁 } ∧ { 𝑁 } ⊆ ℕ0 ) )
16 fss ⊢ ( ( { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ { 𝑁 } ∧ { 𝑁 } ⊆ ℕ0 ) → { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ ℕ0 )
17 15 16 syl ⊢ ( 𝜑 → { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ ℕ0 )
18 2 oveq1d ⊢ ( 𝜑 → ( 𝐾 + 1 ) = ( 0 + 1 ) )
19 0p1e1 ⊢ ( 0 + 1 ) = 1
20 18 19 eqtrdi ⊢ ( 𝜑 → ( 𝐾 + 1 ) = 1 )
21 20 oveq2d ⊢ ( 𝜑 → ( 1 ... ( 𝐾 + 1 ) ) = ( 1 ... 1 ) )
22 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
23 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
24 22 23 syl ⊢ ( 𝜑 → ( 1 ... 1 ) = { 1 } )
25 21 24 eqtrd ⊢ ( 𝜑 → ( 1 ... ( 𝐾 + 1 ) ) = { 1 } )
26 25 eqcomd ⊢ ( 𝜑 → { 1 } = ( 1 ... ( 𝐾 + 1 ) ) )
27 26 feq2d ⊢ ( 𝜑 → ( { ⟨ 1 , 𝑁 ⟩ } : { 1 } ⟶ ℕ0 ↔ { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ) )
28 17 27 mpbid ⊢ ( 𝜑 → { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
29 25 sumeq1d ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = Σ 𝑖 ∈ { 1 } ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) )
30 fvsng ⊢ ( ( 1 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) = 𝑁 )
31 10 1 30 syl2anc ⊢ ( 𝜑 → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) = 𝑁 )
32 1 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
33 31 32 eqeltrd ⊢ ( 𝜑 → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) ∈ ℂ )
34 10 33 jca ⊢ ( 𝜑 → ( 1 ∈ ℕ ∧ ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) ∈ ℂ ) )
35 fveq2 ⊢ ( 𝑖 = 1 → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
36 35 sumsn ⊢ ( ( 1 ∈ ℕ ∧ ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) ∈ ℂ ) → Σ 𝑖 ∈ { 1 } ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
37 34 36 syl ⊢ ( 𝜑 → Σ 𝑖 ∈ { 1 } ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) )
38 10 1 jca ⊢ ( 𝜑 → ( 1 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) )
39 38 30 syl ⊢ ( 𝜑 → ( { ⟨ 1 , 𝑁 ⟩ } ‘ 1 ) = 𝑁 )
40 37 39 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ { 1 } ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 )
41 29 40 eqtrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 )
42 28 41 jca ⊢ ( 𝜑 → ( { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 ) )
43 42 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 ) )
44 snex ⊢ { ⟨ 1 , 𝑁 ⟩ } ∈ V
45 feq1 ⊢ ( 𝑔 = { ⟨ 1 , 𝑁 ⟩ } → ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ↔ { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ) )
46 simpl ⊢ ( ( 𝑔 = { ⟨ 1 , 𝑁 ⟩ } ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑔 = { ⟨ 1 , 𝑁 ⟩ } )
47 46 fveq1d ⊢ ( ( 𝑔 = { ⟨ 1 , 𝑁 ⟩ } ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑔 ‘ 𝑖 ) = ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) )
48 47 sumeq2dv ⊢ ( 𝑔 = { ⟨ 1 , 𝑁 ⟩ } → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) )
49 48 eqeq1d ⊢ ( 𝑔 = { ⟨ 1 , 𝑁 ⟩ } → ( Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 ) )
50 45 49 anbi12d ⊢ ( 𝑔 = { ⟨ 1 , 𝑁 ⟩ } → ( ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) ↔ ( { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 ) ) )
51 50 elabg ⊢ ( { ⟨ 1 , 𝑁 ⟩ } ∈ V → ( { ⟨ 1 , 𝑁 ⟩ } ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 ) ) )
52 44 51 ax-mp ⊢ ( { ⟨ 1 , 𝑁 ⟩ } ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( { ⟨ 1 , 𝑁 ⟩ } : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( { ⟨ 1 , 𝑁 ⟩ } ‘ 𝑖 ) = 𝑁 ) )
53 43 52 sylibr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → { ⟨ 1 , 𝑁 ⟩ } ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
54 4 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
55 53 54 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → { ⟨ 1 , 𝑁 ⟩ } ∈ 𝐴 )
56 7 55 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → if ( 𝐾 = 0 , { ⟨ 1 , 𝑁 ⟩ } , ( 𝑘 ∈ ( 1 ... ( 𝐾 + 1 ) ) ↦ if ( 𝑘 = ( 𝐾 + 1 ) , ( ( 𝑁 + 𝐾 ) − ( 𝑏 ‘ 𝐾 ) ) , if ( 𝑘 = 1 , ( ( 𝑏 ‘ 1 ) − 1 ) , ( ( ( 𝑏 ‘ 𝑘 ) − ( 𝑏 ‘ ( 𝑘 − 1 ) ) ) − 1 ) ) ) ) ) ∈ 𝐴 )
57 56 3 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )