proposition: Lemma Exercise1_12 E f: function_prop f E E -> complete_lattice (sub_order (Zo (\Po E) (fun X => sub (Vfs f X) X))).
proof: Proof. move=> [ff sf tf]; set F:=Zo _ _. move: (sub_osr F) => [or sra]. apply: Exercise1_11b =>// X; rewrite sra => XF. have fp: sub F (\Po E) by apply: Zo_S. have XP: sub X (\Po E) by apply: sub_trans fp. have uE: sub (union X) E. by move=> t /setU_P [y ty yX]; move: (XP _ yX) => /setP_P; apply. exists (union X); apply: (setU_sup1 fp XF); apply: Zo_i; first by apply /setP_P. have pa: sub (union X) (source f) by ue. move=> u /(Vf_image_P ff pa) [v vu ->]. move: vu => /setU_P [y ty yX]; apply /setU_P;ex_tac. move: (XF _ yX) => /Zo_P [_]; apply; apply /(Vf_image_P ff); last by ex_tac. by rewrite sf; move: (XP _ yX) => /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)