proposition: Lemma exercise5_2 a b: bijection (Lf(fun g => Lg a (fun x => direct_image g (singleton x))) (powerset (a \times b)) (gfunctions a (powerset b))).
proof: Proof. set tilde := Lf _ _. apply: lf_bijective. move=> c /setP_P cp; apply:gfunctions_i1 => t ta; apply/setP_P => u. by move /dirim_P => [x _ pb]; move/setXp_P: (cp _ pb) => []. move => u v; set fx := Lg a _; set fy:= Lg a _. move /setP_P => up /setP_P => vp fxy. set_extens x => xs. move /setX_P: (up _ xs) => [px Px Qx]. have: inc (Q x) (Vg fy (P x)). by rewrite -fxy /fx LgV //; apply/dirim_P; ex_tac; rewrite px. by rewrite /fy LgV //; move/dirim_P=> [w /set1_P ->]; rewrite px. move /setX_P: (vp _ xs) => [px Px Qx]. have: inc (Q x) (Vg fx (P x)). by rewrite fxy /fy LgV//; apply/dirim_P; ex_tac; rewrite px. by rewrite /fx LgV//; move/dirim_P=> [w /set1_P ->]; rewrite px. move=> y ys; move: (gfunctions_hi ys)=> [f [fs sf tg gf]]. set (g:=Zo (a \times b) (fun z => inc (Q z) (Vg y (P z)))). have gp: inc g (powerset (a \times b)) by apply/setP_P;apply: Zo_S. rewrite -gf; ex_tac; apply: fgraph_exten; fprops. by aw; rewrite domain_fg. red; rewrite - (proj33 fs) sf => x xa; rewrite LgV // gf;set_extens u. move=> h; apply/dirim_P; exists x; first by fprops. apply: Zo_i; [ apply: (setXp_i xa) | by aw]. rewrite - sf in xa; move: (Vf_target fs xa). by rewrite tg /Vf gf; move/setP_P; apply. by move /dirim_P => [v /set1_P ->] /Zo_P []; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)