| Step | Hyp | Ref
| Expression |
| 1 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → (𝑒 ∈ (1...𝐾) ↦ (𝑒 + Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙))) = (𝑒 ∈ (1...𝐾) ↦ (𝑒 + Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙)))) |
| 2 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑒 = 𝑗) → 𝑒 = 𝑗) |
| 3 | 2 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑒 = 𝑗) → (1...𝑒) = (1...𝑗)) |
| 4 | 3 | sumeq1d 15736 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑒 = 𝑗) → Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) |
| 5 | 2, 4 | oveq12d 7449 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑒 = 𝑗) → (𝑒 + Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) |
| 6 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → 𝑗 ∈ (1...𝐾)) |
| 7 | | ovexd 7466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) ∈ V) |
| 8 | 1, 5, 6, 7 | fvmptd 7023 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → ((𝑒 ∈ (1...𝐾) ↦ (𝑒 + Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙)))‘𝑗) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) |
| 9 | | sticksstones8.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 10 | 9 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → 𝑁 ∈
ℕ0) |
| 11 | | sticksstones8.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 12 | 11 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → 𝐾 ∈
ℕ0) |
| 13 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
| 14 | | sticksstones8.4 |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} |
| 15 | 14 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
| 16 | 15 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} = 𝐴) |
| 17 | 13, 16 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
| 18 | | feq1 6716 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑎 → (𝑔:(1...(𝐾 + 1))⟶ℕ0 ↔
𝑎:(1...(𝐾 +
1))⟶ℕ0)) |
| 19 | | simpl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 = 𝑎 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = 𝑎) |
| 20 | 19 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 = 𝑎 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑔‘𝑖) = (𝑎‘𝑖)) |
| 21 | 20 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = 𝑎 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖)) |
| 22 | 21 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑎 → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁)) |
| 23 | 18, 22 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑎 → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁) ↔ (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁))) |
| 24 | 23 | elabg 3676 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ 𝐴 → (𝑎 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁))) |
| 25 | 13, 24 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁))) |
| 26 | 25 | biimpd 229 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁))) |
| 27 | 17, 26 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁)) |
| 28 | 27 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎:(1...(𝐾 +
1))⟶ℕ0) |
| 29 | 28 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → 𝑎:(1...(𝐾 +
1))⟶ℕ0) |
| 30 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑒 ∈ (1...𝐾) ↦ (𝑒 + Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙))) = (𝑒 ∈ (1...𝐾) ↦ (𝑒 + Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙))) |
| 31 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑙 → (𝑎‘𝑖) = (𝑎‘𝑙)) |
| 32 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑙(𝑎‘𝑖) |
| 33 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝑎‘𝑙) |
| 34 | 31, 32, 33 | cbvsum 15731 |
. . . . . . . . . . 11
⊢
Σ𝑖 ∈
(1...(𝐾 + 1))(𝑎‘𝑖) = Σ𝑙 ∈ (1...(𝐾 + 1))(𝑎‘𝑙) |
| 35 | 27 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁) |
| 36 | 34, 35 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑎‘𝑙) = 𝑁) |
| 37 | 36 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑎‘𝑙) = 𝑁) |
| 38 | 10, 12, 29, 6, 30, 37 | sticksstones7 42153 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → ((𝑒 ∈ (1...𝐾) ↦ (𝑒 + Σ𝑙 ∈ (1...𝑒)(𝑎‘𝑙)))‘𝑗) ∈ (1...(𝑁 + 𝐾))) |
| 39 | 8, 38 | eqeltrrd 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) ∈ (1...(𝑁 + 𝐾))) |
| 40 | 39 | 3expa 1119 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) ∈ (1...(𝑁 + 𝐾))) |
| 41 | | eqid 2737 |
. . . . . 6
⊢ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) |
| 42 | 40, 41 | fmptd 7134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))):(1...𝐾)⟶(1...(𝑁 + 𝐾))) |
| 43 | 9 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) → 𝑁 ∈
ℕ0) |
| 44 | 43 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 < 𝑦) → 𝑁 ∈
ℕ0) |
| 45 | 11 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) → 𝐾 ∈
ℕ0) |
| 46 | 45 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 < 𝑦) → 𝐾 ∈
ℕ0) |
| 47 | 24 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁))) |
| 48 | 47 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁))) |
| 49 | 17, 48 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑎‘𝑖) = 𝑁)) |
| 50 | 49 | simpld 494 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎:(1...(𝐾 +
1))⟶ℕ0) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) → 𝑎:(1...(𝐾 +
1))⟶ℕ0) |
| 52 | 51 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) → 𝑎:(1...(𝐾 +
1))⟶ℕ0) |
| 53 | 52 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 < 𝑦) → 𝑎:(1...(𝐾 +
1))⟶ℕ0) |
| 54 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 < 𝑦) → 𝑥 ∈ (1...𝐾)) |
| 55 | | simplr 769 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 < 𝑦) → 𝑦 ∈ (1...𝐾)) |
| 56 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 < 𝑦) → 𝑥 < 𝑦) |
| 57 | 44, 46, 53, 54, 55, 56, 41 | sticksstones6 42152 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) ∧ 𝑥 < 𝑦) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦)) |
| 58 | 57 | ex 412 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) ∧ 𝑦 ∈ (1...𝐾)) → (𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦))) |
| 59 | 58 | ralrimiva 3146 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 ∈ (1...𝐾)) → ∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦))) |
| 60 | 59 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦))) |
| 61 | 42, 60 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))):(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦)))) |
| 62 | | fzfid 14014 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (1...𝐾) ∈ Fin) |
| 63 | 42, 62 | fexd 7247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ V) |
| 64 | | feq1 6716 |
. . . . . . 7
⊢ (𝑓 = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) → (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ↔ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))):(1...𝐾)⟶(1...(𝑁 + 𝐾)))) |
| 65 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) → (𝑓‘𝑥) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥)) |
| 66 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) → (𝑓‘𝑦) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦)) |
| 67 | 65, 66 | breq12d 5156 |
. . . . . . . . 9
⊢ (𝑓 = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) → ((𝑓‘𝑥) < (𝑓‘𝑦) ↔ ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦))) |
| 68 | 67 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑓 = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) → ((𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ (𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦)))) |
| 69 | 68 | 2ralbidv 3221 |
. . . . . . 7
⊢ (𝑓 = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) → (∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)) ↔ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦)))) |
| 70 | 64, 69 | anbi12d 632 |
. . . . . 6
⊢ (𝑓 = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) → ((𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦))) ↔ ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))):(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦))))) |
| 71 | 70 | elabg 3676 |
. . . . 5
⊢ ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ V → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))):(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦))))) |
| 72 | 63, 71 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} ↔ ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))):(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑥) < ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))‘𝑦))))) |
| 73 | 61, 72 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
| 74 | | sticksstones8.5 |
. . . 4
⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} |
| 75 | 74 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))}) |
| 76 | 73, 75 | eleqtrrd 2844 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) ∈ 𝐵) |
| 77 | | sticksstones8.3 |
. 2
⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) |
| 78 | 76, 77 | fmptd 7134 |
1
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |