feat(finset/basic): Add forall_mem_union (#5064)
Part of [#4943](https://github.com/leanprover-community/mathlib/pull/4943), in order to prove theorems about antichains.
Lemma and proof supplied by [eric-wieser](https://github.com/eric-wieser)
Co-authored-by: Alena Gusakov <agusakov@udel.edu>
