proposition: Lemma inverse_image_family_union {X Y : Type} {f : X -> Y} {g : Y -> X} (F : Family Y) : (forall x, g (f x) = x) -> (forall y, f (g y) = y) -> inverse_image f (FamilyUnion F) = FamilyUnion (inverse_image (inverse_image g) F).
proof: Proof. intros Hgf Hfg. apply Extensionality_Ensembles. split; red; intros. - apply in_inverse_image in H. inversion H. subst. rewrite <- Hgf. exists (inverse_image f S). + constructor. rewrite inverse_image_id_comp. * exact H0. * exact Hfg. + rewrite Hgf. constructor. assumption. - destruct H. apply in_inverse_image in H. constructor. exists (inverse_image g S). + exact H. + constructor. rewrite Hgf. assumption. Qed.
imports: ZornsLemma(IndexedFamilies Powerset_facts)