proposition: Lemma exercise5_f2 f x v w: function f -> source f = (powerset x) -> target f = powerset x -> (forall a b, inc a (powerset x) -> inc b (powerset x) -> sub a b -> sub (Vf f a) (Vf f b)) -> v = intersection(Zo (powerset x) (fun z=> sub (Vf f z) z)) -> w = union(Zo (powerset x) (fun z=> sub z (Vf f z))) -> [/\ Vf f v = v, Vf f w = w & (forall z, sub z x -> Vf f z = z -> (sub v z /\ sub z w))].
proof: Proof. move=> ff sf tf fprop vd wd. set (q:= (Zo (powerset x) (fun z => sub (Vf f z) z))). have xpx: inc x (powerset x) by apply :setP_Ti. have xiq: inc x q. apply: Zo_i=>//. by apply /setP_P; rewrite -tf; apply: Vf_target =>//; rewrite sf. have neq:nonempty q by exists x. set (p:= (Zo (powerset x) (fun z => sub z (Vf f z)))). have fzv:forall z, sub z x -> Vf f z = z -> sub v z. move => z zx Wz. have zq:inc z q by apply: Zo_i; [by apply /setP_P | rewrite Wz; fprops]. by rewrite vd; apply: setI_s1. have fzw:forall z, sub z x -> Vf f z = z -> sub z w. move => z zx Wz. have zp: inc z p by apply: Zo_i; [by apply /setP_P | rewrite Wz; fprops]. by rewrite wd; apply: setU_s1. have qW: forall z, inc z q -> inc (Vf f z) q. move=> z /Zo_P [] /setP_P zx Wzz. have aux := sub_trans Wzz zx. by apply: Zo_i; [ apply/setP_P | apply: fprop => //; apply/setP_P]. have pW: forall z, inc z p -> inc (Vf f z) p. move=> z /Zo_P [] /setP_P zx Wzz. have aux: inc (Vf f z) (powerset x). by rewrite -tf; apply: Vf_target=>//;rewrite sf; apply /setP_P. by apply: Zo_i => //; apply: fprop => //; apply/setP_P. have vp: inc v (powerset x) by apply /setP_P; rewrite vd; apply: setI_s1. have wp: inc w (powerset x). by apply /setP_P; rewrite wd; apply: setU_s2 => y /Zo_P []/setP_P. have pv:sub (Vf f v) v. move=> t tW; rewrite vd; apply: setI_i=>// y /Zo_P [yp sW]. have vy: sub v y by rewrite vd; apply: setI_s1; apply: Zo_i=>//. by apply: sW;apply: (fprop _ _ vp yp vy). have pw:sub w (Vf f w). move=> t; rewrite {1} wd=> /setU_P [y ty] /Zo_P [yp yW]. have tw: (sub y w) by rewrite wd;apply: setU_s1; apply: Zo_i=>//. by move: (fprop _ _ yp wp tw); apply; apply: yW. split. apply: extensionality=>//. have vq: (inc v q) by apply: Zo_i. by move: (qW _ vq)=> aux; rewrite {1} vd;apply: setI_s1. apply: extensionality=>//. have iwp: inc w p by apply: Zo_i. by move: (pW _ iwp) => aux; rewrite {2} wd;apply: setU_s1. move=> z zw wz; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)