Metamath Proof Explorer

Theorem sticksstones17

Description: Extend sticks and stones to finite sets, bijective builder. (Contributed by metakunt, 23-Oct-2024)

Ref Expression
Hypotheses sticksstones17.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones17.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
sticksstones17.3 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
sticksstones17.4 ⊢ 𝐵 = { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) }
sticksstones17.5 ⊢ ( 𝜑 → 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 )
sticksstones17.6 ⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
Assertion sticksstones17 ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )

Proof

Step Hyp Ref Expression
1 sticksstones17.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones17.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones17.3 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
4 sticksstones17.4 ⊢ 𝐵 = { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) }
5 sticksstones17.5 ⊢ ( 𝜑 → 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 )
6 sticksstones17.6 ⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
7 4 eqimssi ⊢ 𝐵 ⊆ { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) }
8 7 a1i ⊢ ( 𝜑 → 𝐵 ⊆ { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) } )
9 8 sseld ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) } ) )
10 9 imp ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) } )
11 vex ⊢ 𝑏 ∈ V
12 feq1 ⊢ ( ℎ = 𝑏 → ( ℎ : 𝑆 ⟶ ℕ0 ↔ 𝑏 : 𝑆 ⟶ ℕ0 ) )
13 simpl ⊢ ( ( ℎ = 𝑏 ∧ 𝑖 ∈ 𝑆 ) → ℎ = 𝑏 )
14 13 fveq1d ⊢ ( ( ℎ = 𝑏 ∧ 𝑖 ∈ 𝑆 ) → ( ℎ ‘ 𝑖 ) = ( 𝑏 ‘ 𝑖 ) )
15 14 sumeq2dv ⊢ ( ℎ = 𝑏 → Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 ) )
16 15 eqeq1d ⊢ ( ℎ = 𝑏 → ( Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 ) = 𝑁 ) )
17 12 16 anbi12d ⊢ ( ℎ = 𝑏 → ( ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑏 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 ) = 𝑁 ) ) )
18 11 17 elab ⊢ ( 𝑏 ∈ { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑏 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 ) = 𝑁 ) )
19 10 18 sylib ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑏 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 ) = 𝑁 ) )
20 19 simpld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 : 𝑆 ⟶ ℕ0 )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑏 : 𝑆 ⟶ ℕ0 )
22 21 3impa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑏 : 𝑆 ⟶ ℕ0 )
23 f1of ⊢ ( 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
24 5 23 syl ⊢ ( 𝜑 → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
26 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
27 26 3impa ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
28 simp3 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑦 ∈ ( 1 ... 𝐾 ) )
29 27 28 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑍 ‘ 𝑦 ) ∈ 𝑆 )
30 22 29 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ∈ ℕ0 )
31 30 3expa ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ∈ ℕ0 )
32 31 fmpttd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) : ( 1 ... 𝐾 ) ⟶ ℕ0 )
33 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
34 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 = 𝑖 ) → 𝑦 = 𝑖 )
35 34 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 = 𝑖 ) → ( 𝑍 ‘ 𝑦 ) = ( 𝑍 ‘ 𝑖 ) )
36 35 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 = 𝑖 ) → ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) = ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) )
37 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑖 ∈ ( 1 ... 𝐾 ) )
38 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) ∈ V )
39 33 36 37 38 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) )
40 39 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) )
41 fveq2 ⊢ ( 𝑠 = ( 𝑍 ‘ 𝑖 ) → ( 𝑏 ‘ 𝑠 ) = ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) )
42 fzfi ⊢ ( 1 ... 𝐾 ) ∈ Fin
43 42 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 ... 𝐾 ) ∈ Fin )
44 5 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 )
45 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑍 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) )
46 nn0sscn ⊢ ℕ0 ⊆ ℂ
47 46 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ℕ0 ⊆ ℂ )
48 fss ⊢ ( ( 𝑏 : 𝑆 ⟶ ℕ0 ∧ ℕ0 ⊆ ℂ ) → 𝑏 : 𝑆 ⟶ ℂ )
49 20 47 48 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 : 𝑆 ⟶ ℂ )
50 49 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑏 ‘ 𝑠 ) ∈ ℂ )
51 41 43 44 45 50 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑠 ∈ 𝑆 ( 𝑏 ‘ 𝑠 ) = Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) )
52 51 eqcomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) = Σ 𝑠 ∈ 𝑆 ( 𝑏 ‘ 𝑠 ) )
53 fveq2 ⊢ ( 𝑠 = 𝑖 → ( 𝑏 ‘ 𝑠 ) = ( 𝑏 ‘ 𝑖 ) )
54 53 cbvsumv ⊢ Σ 𝑠 ∈ 𝑆 ( 𝑏 ‘ 𝑠 ) = Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 )
55 54 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑠 ∈ 𝑆 ( 𝑏 ‘ 𝑠 ) = Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 ) )
56 19 simprd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ 𝑆 ( 𝑏 ‘ 𝑖 ) = 𝑁 )
57 55 56 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑠 ∈ 𝑆 ( 𝑏 ‘ 𝑠 ) = 𝑁 )
58 52 57 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑏 ‘ ( 𝑍 ‘ 𝑖 ) ) = 𝑁 )
59 40 58 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = 𝑁 )
60 32 59 jca ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = 𝑁 ) )
61 fzfid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 1 ... 𝐾 ) ∈ Fin )
62 61 mptexd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ V )
63 feq1 ⊢ ( 𝑔 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) → ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ↔ ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) : ( 1 ... 𝐾 ) ⟶ ℕ0 ) )
64 simpl ⊢ ( ( 𝑔 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑔 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
65 64 fveq1d ⊢ ( ( 𝑔 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑔 ‘ 𝑖 ) = ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) )
66 65 sumeq2dv ⊢ ( 𝑔 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) )
67 66 eqeq1d ⊢ ( 𝑔 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = 𝑁 ) )
68 63 67 anbi12d ⊢ ( 𝑔 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) → ( ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) ↔ ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = 𝑁 ) ) )
69 68 elabg ⊢ ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ V → ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = 𝑁 ) ) )
70 62 69 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ 𝑖 ) = 𝑁 ) ) )
71 60 70 mpbird ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
72 3 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
73 71 72 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ 𝐴 )
74 73 6 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )