Isabelle says yes, but I am not really convinced. Given a map $f$ such that for all sets $A, B$ $A \subseteq B$ implies $f(A) \subseteq f(B)$, then is it always the case that $\bigcup_i f(S_i) = f(\bigcup_i S_i)$? In case it is, why? In case it isn't, where is the error in the next lemma that Isabelle proves?
lemma "(∀ P . ∀ Q . P ⊆ Q ⟶ f`P ⊆ f`Q) ⟹
(f ` (UN x : A . B x) = (UN x : A . f`(B x)))"
by auto
Let $U=\bigcup_iS_i$ and $V=\bigcup_if[S_i]$; we want to show that $f[U]=V$. For each $i$ we have $S_i\subseteq U$, so $f[S_i]\subseteq f[U]$, and hence $V\subseteq f[U]$. On the other hand, if $x\in U$, then $x\in S_i$ for some $I$, so $f(x)\in f[S_i]\subseteq V$, and therefore $f[U]\subseteq V$.