proposition: Lemma Im_Full_set_surj {X Y : Type} (f : X -> Y) : surjective f <-> Full_set = Im Full_set f.
proof: Proof. split. - intros H. apply Extensionality_Ensembles; split; red; intros x ?. 2: { constructor. } destruct (H x) as [y]. subst. apply Im_def. constructor. - intros H y. assert (In (Im Full_set f) y) as Hy. { rewrite <- H. constructor. } inversion Hy; subst; clear Hy. eexists; reflexivity. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(FunctionProperties)