proposition: Lemma le_cardinal_img_inj_ens {X Y : Type} (Z : Type) (f : X -> Y) (U : Ensemble X) : injective_ens f U -> le_cardinal X Z -> le_cardinal (sig (Im U f)) Z.
proof: Proof. intros Hf [g Hg]. assert (forall p : { y : Y | In (Im U f) y }, { x : X | In U x /\ (proj1_sig p) = f x}) as H. { intros [y Hy]. simpl. apply constructive_definite_description. inversion Hy; subst; clear Hy. exists x; split; auto. intros x' []; auto. } exists (compose g (fun p => proj1_sig (H p))). apply injective_compose; auto. clear g Hg. intros p0 p1 Hp. pose proof (proj2_sig (H p0)) as [Hp00 Hp01]. pose proof (proj2_sig (H p1)) as [Hp10 Hp11]. destruct p0 as [y0 Hy0], p1 as [y1 Hy1]. simpl in *. rewrite <- Hp in Hp11. cut (y0 = y1); try congruence. intros. destruct H0. destruct (proof_irrelevance _ Hy0 Hy1). reflexivity. Qed.
imports: Coq(ClassicalChoice) Coq(ProofIrrelevance) Coq(FunctionalExtensionality) Coq(Description) ZornsLemma(FunctionPropertiesEns) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(CSB) ZornsLemma(EnsemblesSpec) ZornsLemma(ZornsLemma) ZornsLemma(EnsemblesImplicit) ZornsLemma(CountableTypes) ZornsLemma(FiniteTypes) ZornsLemma(InfiniteTypes) Coq(RelationClasses)