proposition: Lemma partial_injection_chain_ub: forall S:Ensemble partial_injection, chain partial_injection_ord S -> exists x:partial_injection, forall y:partial_injection, In S y -> partial_injection_ord y x.
proof: Proof. intros. pose (ub_dom := [x:X | exists y:partial_injection, In S y /\ In (pi_dom y) x]). assert (forall x:X, In ub_dom x -> { y:Y | exists z:partial_injection, In S z /\ exists i:In (pi_dom z) x, pi_func z x i = y }). intros. apply constructive_definite_description. destruct H0. destruct H0. destruct H0. exists (pi_func x0 x H1). red; split. exists x0. split. assumption. exists H1. reflexivity. intros. destruct H2. destruct H2. destruct H3. pose proof (H x0 x1 H0 H2). case H4. intro. rewrite <- H3. apply pi_func_ext. assumption. intro. rewrite <- H3. symmetry. apply pi_func_ext. assumption. assert (forall (x1 x2:X) (i1:In ub_dom x1) (i2:In ub_dom x2), proj1_sig (X0 x1 i1) = proj1_sig (X0 x2 i2) -> x1 = x2). intros. destruct X0 in H0. destruct X0 in H0. simpl in H0. destruct H0. destruct e. destruct H0. destruct H1. destruct e0. destruct H2. destruct H3. destruct H1. case (H x0 x4 H0 H2). intro. assert (In (pi_dom x4) x1). apply (pi_dom_inc _ _ H1). assumption. assert (pi_func x4 x1 H4 = pi_func x4 x2 x5). rewrite H3. symmetry. apply pi_func_ext. assumption. apply pi_inj in H5. assumption. intro. assert (In (pi_dom x0) x2). apply (pi_dom_inc _ _ H1). assumption. assert (pi_func x0 x1 x3 = pi_func x0 x2 H4). rewrite <- H3. apply pi_func_ext. assumption. apply pi_inj in H5. assumption. exists (Build_partial_injection ub_dom (fun (x:X) (i:In ub_dom x) => proj1_sig (X0 x i)) H0). intros. constructor. simpl. red; intros. constructor. exists y. tauto. simpl. intros. destruct (X0 x i2). simpl. destruct e. destruct H2. destruct H3. destruct H3. case (H y x1 H1 H2). intro. apply pi_func_ext. assumption. intro. symmetry. apply pi_func_ext. assumption. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec ClassicalChoice ZornsLemma EnsemblesImplicit ProofIrrelevance FunctionalExtensionality Description