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 ⊢ Ⅎ 𝑙 ( 1 ... ( 𝐾 + 1 ) )
35 nfcv ⊢ Ⅎ 𝑖 ( 1 ... ( 𝐾 + 1 ) )
36 nfcv ⊢ Ⅎ 𝑙 ( 𝑎 ‘ 𝑖 )
37 nfcv ⊢ Ⅎ 𝑖 ( 𝑎 ‘ 𝑙 )
38 33 34 35 36 37 cbvsum ⊢ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = Σ 𝑙 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑙 )
39 29 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 )
40 38 39 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → Σ 𝑙 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑙 ) = 𝑁 )
41 40 3adant3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → Σ 𝑙 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑙 ) = 𝑁 )
42 14 15 31 11 32 41 sticksstones7 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( ( 𝑒 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑒 + Σ 𝑙 ∈ ( 1 ... 𝑒 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑗 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
43 13 42 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
44 43 3expa ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑗 ∈ ( 1 ... 𝐾 ) ) → ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
45 eqid ⊢ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) )
46 44 45 fmptd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) )
47 1 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑁 ∈ ℕ0 )
48 47 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑁 ∈ ℕ0 )
49 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝐾 ∈ ℕ0 )
50 49 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝐾 ∈ ℕ0 )
51 26 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } ↔ ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
52 51 biimpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 ∈ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } → ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) ) )
53 19 52 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝑎 ‘ 𝑖 ) = 𝑁 ) )
54 53 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
56 55 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
57 56 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑎 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
58 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ( 1 ... 𝐾 ) )
59 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( 1 ... 𝐾 ) )
60 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
61 48 50 57 58 59 60 45 sticksstones6 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) )
62 61 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) ∧ 𝑦 ∈ ( 1 ... 𝐾 ) ) → ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
63 62 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 ∈ ( 1 ... 𝐾 ) ) → ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
64 63 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
65 46 64 jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) )
66 fzfid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 1 ... 𝐾 ) ∈ Fin )
67 46 66 fexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ V )
68 feq1 ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ↔ ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ) )
69 fveq1 ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) )
70 fveq1 ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) )
71 69 70 breq12d ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) )
72 71 imbi2d ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) )
73 72 2ralbidv ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) )
74 68 73 anbi12d ⊢ ( 𝑓 = ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) → ( ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) ) )
75 74 elabg ⊢ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ V → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) ) )
76 67 75 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } ↔ ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑥 ) < ( ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ‘ 𝑦 ) ) ) ) )
77 65 76 mpbird ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
78 5 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐵 = { 𝑓 ∣ ( 𝑓 : ( 1 ... 𝐾 ) ⟶ ( 1 ... ( 𝑁 + 𝐾 ) ) ∧ ∀ 𝑥 ∈ ( 1 ... 𝐾 ) ∀ 𝑦 ∈ ( 1 ... 𝐾 ) ( 𝑥 < 𝑦 → ( 𝑓 ‘ 𝑥 ) < ( 𝑓 ‘ 𝑦 ) ) ) } )
79 77 78 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑗 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑗 + Σ 𝑙 ∈ ( 1 ... 𝑗 ) ( 𝑎 ‘ 𝑙 ) ) ) ∈ 𝐵 )
80 79 3 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )