proposition: Lemma Exercise6_33q (Ma := Mi alpha): [/\ forall t, inc t N0 -> [/\ inc t c, inc alpha (source (y t))& inc (Vf (y t) alpha) Ma], (forall t1 t2, inc t1 N0 -> inc t2 N0 -> (Vf (y t1) alpha) = (Vf (y t2) alpha) -> t1 = t2), (forall s, inc s Ma -> exists2 t, inc t N0 & s = (Vf (y t) alpha)), sub N0 c & cardinal N0 = c].
proof: Proof. pose Z z := Zo c (fun n => inc alpha (source (y n)) /\ Vf (y n) alpha = z). have znz: forall z, inc z (Mi alpha) -> nonempty (Z z). by move => z /Zo_P [zM [n [nc als zv]]]; exists n; apply: Zo_i. have pa: forall t, inc t N0 -> [/\ inc t c, inc alpha (source (y t)) & inc (Vf (y t) alpha) Ma]. move => t /funI_P [z z1 rz]. move: (rep_i (znz _ z1)); rewrite rz; move /Zo_P => [pa [pb pc]]. split => //; rewrite pc //. have pb: (forall t1 t2, inc t1 N0 -> inc t2 N0 -> (Vf (y t1) alpha) = (Vf (y t2) alpha) -> t1 = t2). move => t1 t2 t1n t2n sv. move: t1n => /funI_P [z z1 rz]. move: (rep_i (znz _ z1)); rewrite rz; move => /Zo_hi [_ pc]. move: t2n => /funI_P [z' z1' rz']. move: (rep_i (znz _ z1')); rewrite rz'; move /Zo_hi => [_ pc']. by move: pc pc' sv; rewrite - {1}rz - {1} rz' -/alpha => -> -> ->. have pc: (forall s, inc s Ma -> exists2 t, inc t N0 & s = Vf (y t) alpha). move => s sm. set u := rep (Z s). have un: inc u N0 by apply /funI_P; rewrite -/Ma; exists s => //. exists u => //. by move: (rep_i (znz _ sm)) => /Zo_P [_ [_ ->]]. split => //. move => t tn; exact: (proj31 (pa _ tn)). set f:= Lf (fun t => Vf (y t) alpha) N0 Ma. have bf: bijection f. by apply: lf_bijective => // t ta; move: (pa _ ta) => [_ _ ok]. have: (source f \Eq target f) by exists f; split => //. rewrite /f; aw; move /card_eqP. by rewrite - (proj32 Exercise6_33o). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)