proposition: Lemma pure_properties_res5 A S: pure_prop1 A S -> pure_prop3 A S -> pure_prop4 S -> pure_prop5 A S -> exists R, [/\ mobile_ext R A, S = (set_of_pure A R) & (forall x z, inc x R -> inc z R -> sub x z -> z = x)].
proof: Proof. move => [nes p1] p3 p4 p5. set R := Zo (\Po A)(fun z => ~(inc z S) /\ forall v, sub v z -> ~ (inc v S) -> v = z). have pa: (forall x z, inc x R -> inc z R-> sub x z -> z = x). move => x z /Zo_P [_ [xs _]] /Zo_hi [_ zp] h. by symmetry; apply: zp. have pb: forall x, inc x R -> sub x A. by move => x /Zo_P [] /setP_P. have pc: ~ inc emptyset R. move /Zo_P =>[ta [tc _]]; case: tc. move: nes => [w ws]; apply:(p4 w emptyset) => //; fprops. have pd: (forall z, inc z R -> finite_set z). move => z => /Zo_P [] /setP_P ta [tb tc]. move: (p5 _ ta tb) => [y [ys fsy nys]]. by rewrite - (tc _ ys nys). have pe: forall M, sub M A -> ~ (inc M S) -> exists2 N, sub N M & inc N R. move => M MA nMS. move: (p5 _ MA nMS) => [y [ym fy nys]]. set T := Zo (\Po y) (fun z => ~ (inc z S)). have tf: (forall x, inc x T -> finite_set x). move => x /Zo_P [] /setP_P xy _. apply: (sub_finite_set xy fy). have yt: inc y T by apply: Zo_i => //; apply /setP_P. move: (Ex4_11_minR_pr tf yt) => [z zt] /Zo_P [ta tb]. move: (sub_trans zt ym) => zM. exists z=> //; apply: Zo_i; first by apply /setP_P; apply: (sub_trans zM MA). move: ta => /Zo_P [_ zs]; split => //. move => v vz nvs; symmetry; apply: tb => //; apply: Zo_i => //. apply /setP_P; apply: (sub_trans vz zt). have pf: mobile_r R. move => M N MR NR; move: (MR) (NR) => /Zo_P [] /setP_P MA [nMS Mm] /Zo_P [] /setP_P NA [nNS Nm] MN z zi. have qa: inc (M \cap N) S. move: (@subsetI2l M N)(@subsetI2r M N) => ta tb. ex_middle ins; move: (Mm _ ta ins) => tc; case: MN; apply: Nm => //; ue. have qb: inc z (M \cup N) by move: zi=> /setI2_P [zm _]; apply /setU2_P; left. move: (p3 _ _ MA NA nMS nNS qa _ qb). set Z := ((M \cup N) -s1 z) => zs. have zc: sub Z (M \cup N) by move => t /setC1_P []. have za: sub Z A by apply: (sub_trans zc) => t; case /setU2_P =>h; fprops. move: (pe _ za zs) => [Z' Z1 Z2]; exists Z'; split => //. apply: (sub_trans Z1 zc). by move => h; move: (Z1 _ h) => /setC1_P[]. have pg: S = set_of_pure A R. set_extens t. move => tS; apply /set_of_pureP;split;fprops. move => x xp => /Zo_P [_ [bad xb]]; case: bad; exact: (p4 _ _ tS xp). move /set_of_pureP => [ta pt]; ex_middle ts. move: (pe _ ta ts) => [N nt nr]; by move: (pt _ nt). by exists R. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)