Metamath Proof Explorer

Theorem sticksstones8

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

Ref Expression
Hypotheses sticksstones8.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones8.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
sticksstones8.3 ⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
sticksstones8.4 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
sticksstones8.5 ⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
Assertion sticksstones8 ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 sticksstones8.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones8.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones8.3 ⊢ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) )
4 sticksstones8.4 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
5 sticksstones8.5 ⊢ 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) }
6 eqidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( 𝑒 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) ) = ( 𝑒 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) ) )
7 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑒 = 𝑗 ) → 𝑒 = 𝑗 )
8 7 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑒 = 𝑗 ) → ( 1 ... 𝑒 ) = ( 1 ... 𝑗 ) )
9 8 sumeq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑒 = 𝑗 ) → Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) = Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) )
10 7 9 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑒 = 𝑗 ) → ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) = ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) )
11 simp3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → 𝑗 ∈ ( 1 ... 𝐾 ) )
12 ovexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ∈ V )
13 6 10 11 12 fvmptd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑒 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑗 ) = ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) )
14 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → 𝑁 ∈ ℕ0 )
15 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → 𝐾 ∈ ℕ0 )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
17 4 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
18 17 eqcomd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } = 𝐴 )
19 16 18 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } )
20 feq1 ⊢ ( 𝑔 = 𝑎 → ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ↔ 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ) )
21 simpl ⊢ ( ( 𝑔 = 𝑎 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑔 = 𝑎 )
22 21 fveq1d ⊢ ( ( 𝑔 = 𝑎 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝑔 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑖 ) )
23 22 sumeq2dv ⊢ ( 𝑔 = 𝑎 → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) )
24 23 eqeq1d ⊢ ( 𝑔 = 𝑎 → ( Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) )
25 20 24 anbi12d ⊢ ( 𝑔 = 𝑎 → ( ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
26 25 elabg ⊢ ( 𝑎 ∈ 𝐴 → ( 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
27 16 26 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
28 27 biimpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } → ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
29 19 28 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) )
30 29 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
31 30 3adant3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
32 eqid ⊢ ( 𝑒 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) ) = ( 𝑒 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) )
33 fveq2 ⊢ ( 𝑖 = 𝑙 → ( 𝑎 ‘ 𝑖 ) = ( 𝑎 ‘ 𝑙 ) )
34 nfcv ⊢ Ⅎ 𝑙 ( 𝑎 ‘ 𝑖 )
35 nfcv ⊢ Ⅎ 𝑖 ( 𝑎 ‘ 𝑙 )
36 33 34 35 cbvsum ⊢ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = Σ 𝑙 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑙 )
37 29 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 )
38 36 37 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → Σ 𝑙 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑙 ) = 𝑁 )
39 38 3adant3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → Σ 𝑙 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑙 ) = 𝑁 )
40 14 15 31 11 32 39 sticksstones7 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑒 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
41 13 40 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
42 41 3expa ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
43 eqid ⊢ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) )
44 42 43 fmptd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
45 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑁 ∈ ℕ0 )
46 45 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑁 ∈ ℕ0 )
47 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝐾 ∈ ℕ0 )
48 47 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝐾 ∈ ℕ0 )
49 26 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
50 49 biimpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } → ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
51 19 50 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) )
52 51 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
54 53 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
55 54 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
56 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 1 ... 𝐾 ) )
57 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( 1 ... 𝐾 ) )
58 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
59 46 48 55 56 57 58 43 sticksstones6 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) )
60 59 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
61 60 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) → ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
62 61 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
63 44 62 jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) )
64 fzfid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 1 ... 𝐾 ) ∈ Fin )
65 44 64 fexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ V )
66 feq1 ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
67 fveq1 ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) )
68 fveq1 ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) )
69 67 68 breq12d ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
70 69 imbi2d ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) )
71 70 2ralbidv ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) )
72 66 71 anbi12d ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) ) )
73 72 elabg ⊢ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ V → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) ) )
74 65 73 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) ) )
75 63 74 mpbird ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
76 5 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
77 75 76 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ 𝐵 )
78 77 3 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )