proposition: Lemma ex4d_orderIr_prop2 A z: uncountable_set A -> cofinal (ex4d_orderr A) z -> countable_set z -> False.
proof: Proof. move => ha [hb hc] hd. move: (finite_subsets_order A);set I := Zo (\Po A) finite_set. move =>[[or sr] pb pc pd pe]. rewrite sr in hc hb. set f := (identity_g z). have df : domain f = z by rewrite /f identity_d. have he: (countable_set (domain f)) by rewrite df. have hf: allf f countable_set. move => x; rewrite df => xz; rewrite/f (identity_ev xz). by move:(hb _ xz) => /Zo_P[_ /finite_is_countable]. move:(countable_union he hf); rewrite setUb_identity. have -> // : union z = A. set_extens t. by move/setU_P =>[y ty yz]; move:(hb _ yz)=> /Zo_P [/setP_P yA _];apply: yA. move => tA; move:(hc _ (pd _ tA)) => [y yz /sub_gleP[_ _ ty]]. apply/setU_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)