proposition: Lemma least_cardinal_exists (P : forall {X : Type} (U : Ensemble X), Prop) {X : Type} (U : Ensemble X) : P U -> exists (Y : Type) (V : Ensemble Y), least_cardinal (@P) V.
proof: Proof. intros HU. pose (F := fun V : Ensemble X => exists (Y : Type) (W : Ensemble Y), P Y W /\ eq_cardinal_ens V W). assert (F U) as HU0. { exists X, U; split; auto; reflexivity. } assert (forall {Y : Type} (W : Ensemble Y), P Y W -> exists (V : Ensemble X), F V /\ le_cardinal_ens V W) as HFmin. { intros Y W HW. destruct (le_cardinal_ens_total U W). { exists U; auto. } destruct H as [[]|]. { exists Empty_set. split. - exists Y, W. split; auto. apply eq_cardinal_ens_empty. apply H0. - apply le_cardinal_ens_Empty_set. } destruct H as [f [Hf0 Hf1]]. exists (Im W f). split. - exists Y, W. split; auto. apply eq_cardinal_ens_sym. apply eq_cardinal_ens_Im_injective. assumption. - apply eq_cardinal_ens_le. apply eq_cardinal_ens_sym. apply eq_cardinal_ens_Im_injective. assumption. } destruct (le_cardinal_ens_wf F) as [V [[Y [W [HV0 HV1]]] HV2]]. { exists U. assumption. } exists Y, W. split; auto. intros Z Q HQ. eapply le_cardinal_ens_Proper_l; eauto. specialize (HFmin Z Q HQ) as [R [HR0 HR1]]. specialize (HV2 R HR0). eapply le_cardinal_ens_transitive; eauto. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)