proposition: Lemma Im_injective {X Y : Type} (f : X -> Y) (U V : Ensemble X) : injective f -> Im U f = Im V f -> U = V.
proof: Proof. intros Hf HUV. apply Extensionality_Ensembles; split; intros x Hx. - assert (In (Im V f) (f x)). { rewrite <- HUV. apply Im_def. assumption. } inversion H; subst; clear H. apply Hf in H1; subst. assumption. - assert (In (Im U f) (f x)). { rewrite HUV. apply Im_def. assumption. } inversion H; subst; clear H. apply Hf in H1; subst. assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)