Erdős Problem 196

Reference: erdosproblems.com/196

theorem Erdos196.erdos_196 : (∀ (f : ℕ ≃ ℕ), ∃ (a : List ℕ), (List.Sorted (fun (x1 x2 : ℕ) => x1 < x2) a ∨ List.Sorted (fun (x1 x2 : ℕ) => x1 > x2) a) ∧ (⇑f '' ↑a.toFinset).IsAPOfLength 4) ↔ sorry

Must every permutation of $\mathbb{N}$, contain a monotone 4-term arithmetic progression?