proposition: Lemma ZornsLemmaForPreorders: exists x:T, premaximal x.
proof: Proof. pose (Requiv (x y:T) := R x y /\ R y x). pose equivalence_Requiv as H. pose (Rquo := quotient Requiv). let Hnew:=fresh"_H" in unshelve refine (let Hnew:=_ in let inducedR := induced_function2arg R H H Hnew in let inducedR_prop := induced_function2arg_correct R H H Hnew in _). - intros. apply propositional_extensionality. split; intros H2. + apply preord_trans with a1; auto. * apply H0. * apply preord_trans with b1; auto. apply H1. + apply preord_trans with a2; auto. * apply H0. * apply preord_trans with b2; auto. apply H1. - clearbody inducedR_prop. fold inducedR in inducedR_prop. assert (exists x:Rquo, maximal inducedR x). + apply ZornsLemma. * constructor; red. ** intros xbar. destruct (quotient_projection_surjective xbar) as [x []]. rewrite inducedR_prop. now apply preord_refl. ** intros xbar ybar zbar ? ?. destruct (quotient_projection_surjective xbar) as [x]. destruct (quotient_projection_surjective ybar) as [y]. destruct (quotient_projection_surjective zbar) as [z]. subst. rewrite inducedR_prop in *. now apply preord_trans with y. ** intros xbar ybar ? ?. destruct (quotient_projection_surjective xbar) as [x]. destruct (quotient_projection_surjective ybar) as [y]. subst. rewrite inducedR_prop in H0, H1. unfold quotient_projection. apply subset_eq_compat, R_impl_equality_of_equiv_class; trivial. now split. * intros Sbar ?. pose (S := inverse_image (quotient_projection _) Sbar). unshelve refine (let H1:=ub_of_chain S _ in _). ** red; intros. pose proof (H0 (quotient_projection _ x) (quotient_projection _ y)). rewrite 2 inducedR_prop in H3. destruct H1, H2. now apply H3. ** destruct H1. exists (quotient_projection _ x). intros ybar ?. destruct (quotient_projection_surjective ybar) as [y]. destruct H3. rewrite inducedR_prop. apply H1. now constructor. + destruct H0 as [xbar], (quotient_projection_surjective xbar) as [x], H1. exists x. red; intros. red in H0. unshelve refine (let H2:=H0 (quotient_projection Requiv y) _ in _). * now rewrite inducedR_prop. * unfold quotient_projection in H2. injection H2; intros. assert (In (equiv_class Requiv x) y). ** rewrite H3. constructor. now apply equiv_refl. ** now destruct H4 as [[? ?]]. Qed.
imports: Coq(ClassicalChoice) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(EnsemblesImplicit) Coq(ProofIrrelevance) Coq(PropExtensionalityFacts) ZornsLemma(InverseImage) ZornsLemma(Quotients) EnsemblesSpec