Erdős Problem 623

Reference: erdosproblems.com/623

theorem Erdos623.erdos_623 : (∀ (X : Type u), Cardinal.mk X = Cardinal.aleph Ordinal.omega0 → ∀ (f : Finset X → X), (∀ (A : Finset X), f A ∉ A) → ∃ (Y : Set X), Y.Infinite ∧ ∀ (B : Finset X), ↑B ⊆ Y → f B ∉ Y) ↔ sorry

Let $X$ be a set of cardinality $\aleph_\omega$ and $f$ be a function from the finite subsets of $X$ to $X$ such that $f(A)\not\in A$ for all $A$. Must there exist an infinite $Y\subseteq X$ that is independent - that is, for all finite $B\subset Y$ we have $f(B)\not\in Y$?