proposition: Lemma Exercise_6_1bis E f: infinite_set E -> function_prop f E E -> exists S, [/\ sub S E, nonempty S, S <> E & sub (Vfs f S) S].
proof: Proof. move => /infinite_setP pa [pb pc pd]; pose g x := Vf f x. have qa: forall x, inc x E -> inc (g x) E. move => x; rewrite - {1} pc - pd /g => xsf; Wtac. case: (emptyset_dichot E). move => ee; rewrite ee in pa. have fce: finite_c (cardinal emptyset) by rewrite cardinal_set0; fprops. case: (finite_not_infinite fce pa). move=> [y0 y0E]; pose y := g y0. have yE: inc y E by apply: qa. pose stable S := forall x, inc x S -> inc (g x) S. pose chained := chained_r (fun a b => a = g b). set S := Zo E (fun z => exists p, [/\ chained p, chain_tail p = y0 & (chain_head p) = z]). have q0: forall p, chained p -> chain_tail p = y0 -> inc (chain_head p) E. elim => c p //= ; [ by move => -> -> | move => Hrec [] -> rb rc]. by apply:qa; apply: Hrec. have q1: sub S E by apply: Zo_S. have q2: nonempty S by exists y; apply/Zo_i => //; exists (chain_pair y y0). have q3: stable S. move => t /Zo_P [tE [c [c1 c2 c3]]]; apply/Zo_P; split => //. by apply: qa. by exists (chain_next (g t) c);split => //; rewrite - c3. have q4:forall S, sub S E -> stable S -> sub (Vfs f S) S. move => s se ss. have aux: sub s (source f) by ue. by move => t /(Vf_image_P pb aux) [u us ->]; apply: ss. case: (equal_or_not S E) => nse; last by exists S;split;fprops. have: inc y0 S by ue. move /Zo_P => [_] [c0 [c1 c2 c3]]. set A:= chain_val c0. have yA: inc y A. by apply /chain_valP; exists (chain_pair y y0) => //;apply chained_prop1. have sa: stable A. move => s /chain_valP [p p1 ->]; case: (chained_prop2 c1 p1) => sq. rewrite sq c3; exact yA. by apply /chain_valP; exists (chain_next (g (chain_head p)) p). have sas: sub A E. move => t /chain_valP [p p1 p2]. move: (sub_chainedP p1 c1); rewrite c2 p2; move => [xx1 xx2]. by apply: q0. have ae: A <> E. move => bad. have : finite_set A by apply: chain_val_finite. by rewrite bad => fse; exact:(finite_not_infinite fse pa). exists A;split => //; [ by exists y | by apply: q4]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)