Metamath Proof Explorer

Theorem sticksstones18

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

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

Proof

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