proposition: Lemma image_family_union (X Y : Type) (F : Family X) (f : X -> Y) : Im (FamilyUnion F) f = FamilyUnion (Im F (fun U => Im U f)).
proof: Proof. apply Extensionality_Ensembles; split; red; intros. - inversion_clear H. subst. inversion_clear H0. exists (Im S f). { exists S; auto. } apply Im_def. assumption. - inversion_clear H. inversion_clear H0. subst. inversion_clear H1. subst. apply Im_def. exists x0; auto. Qed.
imports: Coq(Classical_Prop) Coq(Classical_sets) Coq(Morphisms) ZornsLemma(Image ImageImplicit) ZornsLemma(EnsemblesImplicit)