proposition: Lemma exercise6_3 a x: sub a x -> bijection (intersection_with_canon x a).
proof: Proof. move=> ax. have ta: lf_axiom (intersection2 a) (powerset x) (powerset x). move=> y /setP_P ay; apply /setP_i;apply: sub_trans ay ;apply: subsetI2r. have fai: function (intersection_with x a) by apply: lf_function. move:(graph_ea_equivalence fai). set r:= equivalence_associated (intersection_with x a); move => [er sr]. have rr: forall u v, related r u v <-> [/\ inc u (powerset x), inc v (powerset x) & a \cap u = a \cap v]. move => u v; split. move/(ea_relatedP fai); rewrite lf_source; move => [pa pb]. by rewrite !LfV. move => [pa pb pc]; apply/(ea_relatedP fai). by rewrite /intersection_with !LfV//; aw. have aux: forall y, sub y a -> y = a \cap y by move => y; move/setI2id_Pr. apply: lf_bijective. move=> y /setP_P=> ya;set w:= Zo _ _ . have new: nonempty w. exists y;apply: Zo_i; [apply/setP_P; apply: (sub_trans ya ax) | auto]. have swp: sub w (powerset x) by apply: Zo_S. have rp: inc (rep w) (powerset x) by apply: swp;apply: rep_i. apply /(setQ_P er); split => //. by move: rp;rewrite sr /intersection_with; aw. have ira: (a \cap (rep w) = y). have: (inc (rep w) w) by apply: rep_i. by move /Zo_hi => ->. set_extens z. move=> zw; apply /(class_P er); apply /rr;split => //; first by apply:swp. by rewrite ira; move /Zo_P: zw => []. by move/(class_P er)/rr => [pa pb pc]; apply: Zo_i => //; rewrite -pc ira. move=> u v /setP_P ua /setP_P va; set fs:= Zo _ _ => eql. have iua: u = a \cap u by apply: aux. have: inc u fs by apply: Zo_i => //; apply/setP_P; apply:(sub_trans ua ax). by rewrite eql; move/ Zo_hi => ->. move=> y /(setQ_P er) cy. have ip: inc (a \cap (rep y)) (powerset a) by apply/setP_P; apply subsetI2l. move: sr; rewrite lf_source => sr2. ex_tac; symmetry;set_extens t. move /Zo_P => []; move /setP_P => pd pe. apply: (rel_in_class2 er cy); apply/rr;split => //; last by apply /setP_P. rewrite - sr2; exact (proj1 cy). move => ty; apply /Zo_i; first by rewrite - sr2; apply: (sub_class_sr er cy ty). by move: (rel_in_class er cy ty) => /rr [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)