Metamath Proof Explorer

Theorem sticksstones19

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

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

Proof

Step Hyp Ref Expression
1 sticksstones19.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones19.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones19.3 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
4 sticksstones19.4 ⊢ 𝐵 = { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) }
5 sticksstones19.5 ⊢ ( 𝜑 → 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 )
6 sticksstones19.6 ⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
7 sticksstones19.7 ⊢ 𝐺 = ( 𝑏 ∈ 𝐵 ↦ ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
8 1 2 3 4 5 6 sticksstones18 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9 1 2 3 4 5 7 sticksstones17 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
10 7 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝐺 = ( 𝑏 ∈ 𝐵 ↦ ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ) )
11 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑐 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑏 = ( 𝐹 ‘ 𝑐 ) )
12 11 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑐 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) )
13 12 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑐 ) ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
14 8 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑐 ) ∈ 𝐵 )
15 fzfid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 1 ... 𝐾 ) ∈ Fin )
16 15 mptexd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ V )
17 10 13 14 16 fvmptd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑐 ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
18 6 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) )
19 18 fveq1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝐹 ‘ 𝑐 ) = ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) )
20 19 fveq1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) = ( ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) )
21 20 3expa ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) = ( ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) )
22 21 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
23 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) )
24 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 = 𝑐 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑎 = 𝑐 )
25 24 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 = 𝑐 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) = ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) )
26 25 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑎 = 𝑐 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
27 simplr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑐 ∈ 𝐴 )
28 fzfid ⊢ ( 𝜑 → ( 1 ... 𝐾 ) ∈ Fin )
29 f1oenfi ⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 ) → ( 1 ... 𝐾 ) ≈ 𝑆 )
30 28 5 29 syl2anc ⊢ ( 𝜑 → ( 1 ... 𝐾 ) ≈ 𝑆 )
31 30 ensymd ⊢ ( 𝜑 → 𝑆 ≈ ( 1 ... 𝐾 ) )
32 enfii ⊢ ( ( ( 1 ... 𝐾 ) ∈ Fin ∧ 𝑆 ≈ ( 1 ... 𝐾 ) ) → 𝑆 ∈ Fin )
33 28 31 32 syl2anc ⊢ ( 𝜑 → 𝑆 ∈ Fin )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑆 ∈ Fin )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑆 ∈ Fin )
36 35 mptexd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ∈ V )
37 23 26 27 36 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
38 37 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) = ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ‘ ( 𝑍 ‘ 𝑦 ) ) )
39 38 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
40 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 = ( 𝑍 ‘ 𝑦 ) ) → 𝑥 = ( 𝑍 ‘ 𝑦 ) )
42 41 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 = ( 𝑍 ‘ 𝑦 ) ) → ( ◡ 𝑍 ‘ 𝑥 ) = ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) )
43 42 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 = ( 𝑍 ‘ 𝑦 ) ) → ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) = ( 𝑐 ‘ ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
44 f1of ⊢ ( 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
45 5 44 syl ⊢ ( 𝜑 → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑍 : ( 1 ... 𝐾 ) ⟶ 𝑆 )
47 46 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑍 ‘ 𝑦 ) ∈ 𝑆 )
48 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑐 ‘ ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ V )
49 40 43 47 48 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ‘ ( 𝑍 ‘ 𝑦 ) ) = ( 𝑐 ‘ ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
50 49 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ) )
51 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 )
52 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑦 ∈ ( 1 ... 𝐾 ) )
53 f1ocnvfv1 ⊢ ( ( 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) = 𝑦 )
54 51 52 53 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) = 𝑦 )
55 54 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑐 ‘ ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑐 ‘ 𝑦 ) )
56 55 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑐 ‘ 𝑦 ) ) )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ 𝐴 )
58 3 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
59 57 58 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
60 vex ⊢ 𝑐 ∈ V
61 feq1 ⊢ ( 𝑔 = 𝑐 → ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ↔ 𝑐 : ( 1 ... 𝐾 ) ⟶ ℕ0 ) )
62 simpl ⊢ ( ( 𝑔 = 𝑐 ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → 𝑔 = 𝑐 )
63 62 fveq1d ⊢ ( ( 𝑔 = 𝑐 ∧ 𝑖 ∈ ( 1 ... 𝐾 ) ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑐 ‘ 𝑖 ) )
64 63 sumeq2dv ⊢ ( 𝑔 = 𝑐 → Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑐 ‘ 𝑖 ) )
65 64 eqeq1d ⊢ ( 𝑔 = 𝑐 → ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑐 ‘ 𝑖 ) = 𝑁 ) )
66 61 65 anbi12d ⊢ ( 𝑔 = 𝑐 → ( ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑐 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑐 ‘ 𝑖 ) = 𝑁 ) ) )
67 60 66 elab ⊢ ( 𝑐 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑐 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑐 ‘ 𝑖 ) = 𝑁 ) )
68 59 67 sylib ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑐 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑐 ‘ 𝑖 ) = 𝑁 ) )
69 68 simpld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 : ( 1 ... 𝐾 ) ⟶ ℕ0 )
70 ffn ⊢ ( 𝑐 : ( 1 ... 𝐾 ) ⟶ ℕ0 → 𝑐 Fn ( 1 ... 𝐾 ) )
71 69 70 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 Fn ( 1 ... 𝐾 ) )
72 dffn5 ⊢ ( 𝑐 Fn ( 1 ... 𝐾 ) ↔ 𝑐 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑐 ‘ 𝑦 ) ) )
73 71 72 sylib ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → 𝑐 = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑐 ‘ 𝑦 ) ) )
74 73 eqcomd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑐 ‘ 𝑦 ) ) = 𝑐 )
75 56 74 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ) = 𝑐 )
76 50 75 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝑥 ∈ 𝑆 ↦ ( 𝑐 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) = 𝑐 )
77 39 76 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) = 𝑐 )
78 22 77 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( ( 𝐹 ‘ 𝑐 ) ‘ ( 𝑍 ‘ 𝑦 ) ) ) = 𝑐 )
79 17 78 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑐 ) ) = 𝑐 )
80 79 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ 𝐴 ( 𝐺 ‘ ( 𝐹 ‘ 𝑐 ) ) = 𝑐 )
81 6 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) )
82 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑎 = ( 𝐺 ‘ 𝑑 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑎 = ( 𝐺 ‘ 𝑑 ) )
83 82 fveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑎 = ( 𝐺 ‘ 𝑑 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑑 ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) )
84 83 mpteq2dva ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑎 = ( 𝐺 ‘ 𝑑 ) ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑎 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑑 ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
85 9 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑑 ) ∈ 𝐴 )
86 33 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑆 ∈ Fin )
87 86 mptexd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑑 ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ∈ V )
88 81 84 85 87 fvmptd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑑 ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
89 7 a1i ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐺 = ( 𝑏 ∈ 𝐵 ↦ ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ) )
90 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑏 = 𝑑 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑏 = 𝑑 )
91 90 fveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑏 = 𝑑 ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) = ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) )
92 91 mpteq2dva ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑏 = 𝑑 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑏 ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
93 simplr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑑 ∈ 𝐵 )
94 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 1 ... 𝐾 ) ∈ Fin )
95 94 mptexd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ∈ V )
96 89 92 93 95 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑑 ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
97 96 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐺 ‘ 𝑑 ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) = ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) )
98 97 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑑 ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
99 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) )
100 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = ( ◡ 𝑍 ‘ 𝑥 ) ) → 𝑦 = ( ◡ 𝑍 ‘ 𝑥 ) )
101 100 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = ( ◡ 𝑍 ‘ 𝑥 ) ) → ( 𝑍 ‘ 𝑦 ) = ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) )
102 101 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) ∧ 𝑦 = ( ◡ 𝑍 ‘ 𝑥 ) ) → ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) = ( 𝑑 ‘ ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
103 f1ocnv ⊢ ( 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 → ◡ 𝑍 : 𝑆 –1-1-onto→ ( 1 ... 𝐾 ) )
104 5 103 syl ⊢ ( 𝜑 → ◡ 𝑍 : 𝑆 –1-1-onto→ ( 1 ... 𝐾 ) )
105 f1of ⊢ ( ◡ 𝑍 : 𝑆 –1-1-onto→ ( 1 ... 𝐾 ) → ◡ 𝑍 : 𝑆 ⟶ ( 1 ... 𝐾 ) )
106 104 105 syl ⊢ ( 𝜑 → ◡ 𝑍 : 𝑆 ⟶ ( 1 ... 𝐾 ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ◡ 𝑍 : 𝑆 ⟶ ( 1 ... 𝐾 ) )
108 107 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( ◡ 𝑍 ‘ 𝑥 ) ∈ ( 1 ... 𝐾 ) )
109 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑑 ‘ ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ∈ V )
110 99 102 108 109 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) = ( 𝑑 ‘ ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) )
111 110 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑑 ‘ ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) )
112 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 )
113 simpr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
114 f1ocnvfv2 ⊢ ( ( 𝑍 : ( 1 ... 𝐾 ) –1-1-onto→ 𝑆 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) = 𝑥 )
115 112 113 114 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) = 𝑥 )
116 115 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑑 ‘ ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = ( 𝑑 ‘ 𝑥 ) )
117 116 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑑 ‘ ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑑 ‘ 𝑥 ) ) )
118 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 ∈ 𝐵 )
119 4 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝐵 = { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) } )
120 118 119 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 ∈ { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) } )
121 vex ⊢ 𝑑 ∈ V
122 feq1 ⊢ ( ℎ = 𝑑 → ( ℎ : 𝑆 ⟶ ℕ0 ↔ 𝑑 : 𝑆 ⟶ ℕ0 ) )
123 simpl ⊢ ( ( ℎ = 𝑑 ∧ 𝑖 ∈ 𝑆 ) → ℎ = 𝑑 )
124 123 fveq1d ⊢ ( ( ℎ = 𝑑 ∧ 𝑖 ∈ 𝑆 ) → ( ℎ ‘ 𝑖 ) = ( 𝑑 ‘ 𝑖 ) )
125 124 sumeq2dv ⊢ ( ℎ = 𝑑 → Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = Σ 𝑖 ∈ 𝑆 ( 𝑑 ‘ 𝑖 ) )
126 125 eqeq1d ⊢ ( ℎ = 𝑑 → ( Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ 𝑆 ( 𝑑 ‘ 𝑖 ) = 𝑁 ) )
127 122 126 anbi12d ⊢ ( ℎ = 𝑑 → ( ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑑 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑑 ‘ 𝑖 ) = 𝑁 ) ) )
128 121 127 elab ⊢ ( 𝑑 ∈ { ℎ ∣ ( ℎ : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( ℎ ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑑 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑑 ‘ 𝑖 ) = 𝑁 ) )
129 120 128 sylib ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑑 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑑 ‘ 𝑖 ) = 𝑁 ) )
130 129 simpld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 : 𝑆 ⟶ ℕ0 )
131 ffn ⊢ ( 𝑑 : 𝑆 ⟶ ℕ0 → 𝑑 Fn 𝑆 )
132 130 131 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 Fn 𝑆 )
133 dffn5 ⊢ ( 𝑑 Fn 𝑆 ↔ 𝑑 = ( 𝑥 ∈ 𝑆 ↦ ( 𝑑 ‘ 𝑥 ) ) )
134 132 133 sylib ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → 𝑑 = ( 𝑥 ∈ 𝑆 ↦ ( 𝑑 ‘ 𝑥 ) ) )
135 134 eqcomd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑑 ‘ 𝑥 ) ) = 𝑑 )
136 117 135 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑑 ‘ ( 𝑍 ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) ) = 𝑑 )
137 111 136 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝑦 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑑 ‘ ( 𝑍 ‘ 𝑦 ) ) ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = 𝑑 )
138 98 137 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐺 ‘ 𝑑 ) ‘ ( ◡ 𝑍 ‘ 𝑥 ) ) ) = 𝑑 )
139 88 138 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) = 𝑑 )
140 139 ralrimiva ⊢ ( 𝜑 → ∀ 𝑑 ∈ 𝐵 ( 𝐹 ‘ ( 𝐺 ‘ 𝑑 ) ) = 𝑑 )
141 8 9 80 140 2fvidf1od ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )