proposition: Lemma iirel_classP f r: iirel_axioms f r -> forall x, (classp (inv_image_relation f r) x <-> exists y, [/\ classp r y, nonempty (y \cap (Imf f)) & x = Vfi f y]).
proof: Proof. move=> ia; move: (ia) => [ff er tf]. have [pa sir] := (iirel_relation ia). move => x; split. move => clix; move: (clix)=> []; rewrite sir => sa sb. have iWs: inc (Vf f (rep x)) (substrate r) by rewrite tf; Wtac. exists (class r (Vf f (rep x))); split. - by apply: class_class. - exists (Vf f (rep x)); apply: setI2_i; [ fprops | Wtac ]. - set_extens t. rewrite {1} sb => /(class_P pa) /(iirel_relatedP ia) [ysf tsf ryt]. apply/(iim_fun_P); exists (Vf f t); [ by apply /class_P | Wtac]. move /(iim_fun_P) => [u uc Jg]; rewrite sb; apply /(class_P pa). apply /(iirel_relatedP ia);split => //; first by Wtac. by rewrite - (Vf_pr ff Jg); apply /(class_P er). move=> [y [cy [u ui] xi]]; move: cy => [c1 c2]. move: ui => /setI2_P [uy] /(Imf_P ff) [v vsf uw]. have vx: inc v x by rewrite xi; apply /(iim_fun_P); ex_tac; rewrite uw; Wtac. have qc: related r (rep y) (Vf f v) by rewrite - uw;apply /class_P => //; ue. suff: x = class (inv_image_relation f r) v. move => ->; apply: class_class => //; ue. set_extens t. rewrite xi => /(iim_fun_P) [z' z'y Jg2]. apply/(class_P pa); apply /(iirel_relatedP ia);split => //; first by Wtac. have pb: related r (rep y) z' by apply /(class_P er); ue. rewrite - (Vf_pr ff Jg2); equiv_tac. move /(class_P pa) => /(iirel_relatedP ia) [_ qa qb]. rewrite xi; apply /(iim_fun_P); exists (Vf f t) => //; last by Wtac. rewrite c2; apply /class_P => //; equiv_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)