proposition: Lemma cardinals_unbounded {X : Type} (U : Ensemble X) : lt_cardinal_ens U (fun V : Ensemble X => Included V U).
proof: Proof. split. - right. exists Singleton. split. + intros x Hx y Hy. inversion Hy; subst; clear Hy. assumption. + intros x0 x1 Hx0 Hx1 Hx. apply Singleton_injective in Hx. assumption. - intros H. apply eq_cardinal_ens_sym in H. destruct H as [[H _]|[f Hf]]. + apply (H Empty_set). + destruct Hf as [Hf0 [Hf1 Hf2]]. apply (cantor_diag2 U f). assumption. 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)