proposition: Lemma iclosed_normal_fun f x y: ordinalp x -> ordinalp y -> normal_function f x y -> iclosed_set (Imf f).
proof: Proof. move => ox oy nf; move: (nf)=> [[ff sf tf] pb pc]; split. by move =>t /(Imf_Starget ff); rewrite tf => /(Os_ordinal oy). move => F fr [w wf]. set G := Zo (source f) (fun z => inc (Vf f z) F). have sgx: sub G x by rewrite - sf; apply:Zo_S. have neG: nonempty G. move /(Imf_P ff): (fr _ wf) => [u uf uv]; exists u; apply:Zo_i => //; ue. have le1:=(ord_ub_sup1 ox sgx). have sG: sub G (source f) by ue. case: (equal_or_not (\osup G) x) => sx. have og:= Os_sub (Os_ordinal ox) sgx. rewrite - sf in pb. left; apply: ord_sup_1cofinal; first split => //; last first. by move =>t /(Imf_Starget ff); rewrite tf => /(Os_ordinal oy). move => b /(Imf_P ff) [u usf ->]. have ua': u <o \osup G by rewrite sx; apply /(oltP ox); ue. move: (olt_sup og ua') => [v vg uv]. move /Zo_hi: (vg) => vf;ex_tac; exact: (proj1 (pb _ _ usf (Zo_S vg) uv)). have <-: Vfs f G = F. set_extens t; first by move /(Vf_image_P ff sG)=> [u /Zo_hi h ->]. move => tF; apply /(Vf_image_P ff sG). move /(Imf_P ff): (fr _ tF)=> [u usf uv]; exists u => //. apply: Zo_i => //; ue. case: (normal_function_equiv ox oy nf sgx neG) => // <-; right. apply /(Imf_P ff); exists (\osup G) => //; rewrite sf. by apply/(oltP ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)