Theory Replacement_Instances

section‹More Instances of Replacement›

theory Replacement_Instances
  imports
    Separation_Instances
    Transitive_Models.Pointed_DC_Relative
begin

lemma composition_fm_type[TC]: "a0  ω  a1  ω  a2  ω 
   composition_fm(a0,a1,a2)  formula"
  unfolding composition_fm_def by simp

arity_theorem for "composition_fm"

definition is_omega_funspace :: "[io,i,i,i]o" where
  "is_omega_funspace(N,B,n,z)   o[N]. omega(N,o)  no  is_funspace(N, n, B, z)"

synthesize "omega_funspace" from_definition "is_omega_funspace" assuming "nonempty"
arity_theorem for "omega_funspace_fm"

definition HAleph_wfrec_repl_body where
  "HAleph_wfrec_repl_body(N,mesa,x,z)  y[N].
                   pair(N, x, y, z) 
                   (g[N].
                       (u[N].
                           u  g 
                           (a[N].
                               y[N].
                                  ax[N].
                                     sx[N].
                                        r_sx[N].
                                           f_r_sx[N].
                                              pair(N, a, y, u) 
                                              pair(N, a, x, ax) 
                                              upair(N, a, a, sx) 
                                              pre_image(N, mesa, sx, r_sx) 
      restriction(N, g, r_sx, f_r_sx)  ax  mesa  is_HAleph(N, a, f_r_sx, y))) 
                       is_HAleph(N, x, g, y))"

(* MOVE THIS to an appropriate place *)
arity_theorem for "ordinal_fm"
arity_theorem for "is_Limit_fm"
arity_theorem for "empty_fm"
arity_theorem for "fun_apply_fm"

synthesize "HAleph_wfrec_repl_body" from_definition assuming "nonempty"
arity_theorem for "HAleph_wfrec_repl_body_fm"

definition dcwit_repl_body where
  "dcwit_repl_body(N,mesa,A,a,s,R)  λx z. y[N]. pair(N, x, y, z) 
                                is_wfrec
                                 (N, λn f. is_nat_case
                                             (N, a,
                                              λm bmfm.
                                                 fm[N].
                                                    cp[N].
                                                       is_apply(N, f, m, fm) 
                                                       is_Collect(N, A, λx. fmx[N]. (N(x)  fmx  R)  pair(N, fm, x, fmx), cp) 
                                                       is_apply(N, s, cp, bmfm),
                                              n),
                                  mesa, x, y)"

manual_schematic for "dcwit_repl_body" assuming "nonempty"
  unfolding dcwit_repl_body_def
  by (rule iff_sats is_nat_case_iff_sats is_eclose_iff_sats sep_rules | simp)+

synthesize "dcwit_repl_body" from_schematic

definition dcwit_aux_fm where
  "dcwit_aux_fm(A,s,R)  (⋅∃4`2 is 0 
               (⋅∃Collect_fm
                   (succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(A)))))))))),
                    (⋅∃0 
                       succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(R))))))))))))  
                       pair_fm(3, 1, 0) ⋅),
                    0) 
                   succ(succ(succ(succ(succ(succ(succ(succ(succ(succ(s))))))))))`0 is 2⋅)⋅)"

arity_theorem for "dcwit_aux_fm"

lemma dcwit_aux_fm_type[TC]: "A  ω  s  ω  R  ω  dcwit_aux_fm(A,s,R)  formula"
  by (simp_all add: dcwit_aux_fm_def)

definition is_nat_case_dcwit_aux_fm where
  "is_nat_case_dcwit_aux_fm(A,a,s,R)  is_nat_case_fm
           (succ(succ(succ(succ(succ(succ(a)))))),dcwit_aux_fm(A,s,R),
            2, 0)"

lemma is_nat_case_dcwit_aux_fm_type[TC]: "A  ω  a  ω  s  ω  R  ω  is_nat_case_dcwit_aux_fm(A,a,s,R)  formula"
  by (simp_all add: is_nat_case_dcwit_aux_fm_def)

manual_arity for "is_nat_case_dcwit_aux_fm"
  unfolding is_nat_case_dcwit_aux_fm_def
  by (rule arity_dcwit_aux_fm[THEN [6] arity_is_nat_case_fm]) simp_all

manual_arity for "dcwit_repl_body_fm"
  using arity_is_nat_case_dcwit_aux_fm[THEN [6] arity_is_wfrec_fm]
  unfolding dcwit_repl_body_fm_def  is_nat_case_dcwit_aux_fm_def dcwit_aux_fm_def
  by (auto simp add: arity(1-33))

lemma arity_dcwit_repl_body: "arity(dcwit_repl_body_fm(6,5,4,3,2,0,1)) = 7"
  by (simp_all add: FOL_arities arity_dcwit_repl_body_fm ord_simp_union)

definition fst2_snd2
  where "fst2_snd2(x)  fst(fst(x)), snd(snd(x))"

relativize functional "fst2_snd2" "fst2_snd2_rel"
relationalize "fst2_snd2_rel" "is_fst2_snd2"

lemma (in M_trivial) fst2_snd2_abs:
  assumes "M(x)" "M(res)"
  shows "is_fst2_snd2(M, x, res)  res = fst2_snd2(x)"
  unfolding is_fst2_snd2_def fst2_snd2_def
  using fst_rel_abs snd_rel_abs fst_abs snd_abs assms
  by simp

synthesize "is_fst2_snd2" from_definition assuming "nonempty"
arity_theorem for "is_fst2_snd2_fm"

definition sndfst_fst2_snd2
  where "sndfst_fst2_snd2(x)  snd(fst(x)), fst(fst(x)), snd(snd(x))"

relativize functional "sndfst_fst2_snd2" "sndfst_fst2_snd2_rel"
relationalize "sndfst_fst2_snd2_rel" "is_sndfst_fst2_snd2"
synthesize "is_sndfst_fst2_snd2" from_definition assuming "nonempty"
arity_theorem for "is_sndfst_fst2_snd2_fm"

definition order_eq_map where
  "order_eq_map(M,A,r,a,z)  x[M]. g[M]. mx[M]. par[M].
             ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
             pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g)"

synthesize "order_eq_map" from_definition assuming "nonempty"
arity_theorem for "is_ord_iso_fm"
arity_theorem for "order_eq_map_fm"

(* Banach *)
synthesize "is_banach_functor" from_definition assuming "nonempty"
arity_theorem for "is_banach_functor_fm"

definition banach_body_iterates where
  "banach_body_iterates(M,X,Y,f,g,W,n,x,z) 
y[M].
                   pair(M, x, y, z) 
                   (fa[M].
                       (z[M].
                           z  fa 
                           (xa[M].
                               y[M].
                                  xaa[M].
                                     sx[M].
                                        r_sx[M].
                                           f_r_sx[M]. sn[M]. msn[M]. successor(M,n,sn) 
                                              membership(M,sn,msn) 
                                              pair(M, xa, y, z) 
                                              pair(M, xa, x, xaa) 
                                              upair(M, xa, xa, sx) 
                                              pre_image(M, msn, sx, r_sx) 
                                              restriction(M, fa, r_sx, f_r_sx) 
                                              xaa  msn 
                                              (empty(M, xa)  y = W) 
                                              (m[M].
                                                  successor(M, m, xa) 
                                                  (gm[M].
                                                      is_apply(M, f_r_sx, m, gm)  is_banach_functor(M, X, Y, f, g, gm, y))) 
                                              (is_quasinat(M, xa)  empty(M, y)))) 
                       (empty(M, x)  y = W) 
                       (m[M].
                           successor(M, m, x) 
                           (gm[M]. is_apply(M, fa, m, gm)  is_banach_functor(M, X, Y, f, g, gm, y))) 
                       (is_quasinat(M, x)  empty(M, y)))"

synthesize "is_quasinat" from_definition assuming "nonempty"
arity_theorem for "is_quasinat_fm"

synthesize "banach_body_iterates" from_definition assuming "nonempty"
arity_theorem for "banach_body_iterates_fm"

definition banach_is_iterates_body where
  "banach_is_iterates_body(M,X,Y,f,g,W,n,y)  om[M]. omega(M,om)  n  om 
             (sn[M].
                 msn[M].
                    successor(M, n, sn) 
                    membership(M, sn, msn) 
                    (fa[M].
                        (z[M].
                            z  fa 
                            (x[M].
                                y[M].
                                   xa[M].
                                      sx[M].
                                         r_sx[M].
                                            f_r_sx[M].
                                               pair(M, x, y, z) 
                                               pair(M, x, n, xa) 
                                               upair(M, x, x, sx) 
                                               pre_image(M, msn, sx, r_sx) 
                                               restriction(M, fa, r_sx, f_r_sx) 
                                               xa  msn 
                                               (empty(M, x)  y = W) 
                                               (m[M].
                                                   successor(M, m, x) 
                                                   (gm[M].
                                                       fun_apply(M, f_r_sx, m, gm)  is_banach_functor(M, X, Y, f, g, gm, y))) 
                                               (is_quasinat(M, x)  empty(M, y)))) 
                        (empty(M, n)  y = W) 
                        (m[M].
                            successor(M, m, n) 
                            (gm[M]. fun_apply(M, fa, m, gm)  is_banach_functor(M, X, Y, f, g, gm, y))) 
                        (is_quasinat(M, n)  empty(M, y))))"

synthesize "banach_is_iterates_body" from_definition assuming "nonempty"
arity_theorem for "banach_is_iterates_body_fm"

(* (##M)(f) ⟹ strong_replacement(##M, λx y. y = ⟨x, transrec(x, λa g. f ` (g `` a))⟩) *)

definition trans_apply_image where
  "trans_apply_image(f)  λa g. f ` (g `` a)"

relativize functional "trans_apply_image" "trans_apply_image_rel"
relationalize "trans_apply_image" "is_trans_apply_image"

(* MOVE THIS to an appropriate place *)
schematic_goal arity_is_recfun_fm[arity]:
  "p  formula  a  ω  z  ω  r  ω  arity(is_recfun_fm(p, a, z ,r)) = ?ar"
  unfolding is_recfun_fm_def
  by (simp add:arity) (* clean simpset from arities, use correct attrib *)
    (* Don't know why it doesn't use the theorem at 🗏‹Arities› *)
schematic_goal arity_is_wfrec_fm[arity]:
  "p  formula  a  ω  z  ω  r  ω  arity(is_wfrec_fm(p, a, z ,r)) = ?ar"
  unfolding is_wfrec_fm_def
  by (simp add:arity)
schematic_goal arity_is_transrec_fm[arity]:
  "p  formula  a  ω  z  ω  arity(is_transrec_fm(p, a, z)) = ?ar"
  unfolding is_transrec_fm_def
  by (simp add:arity)

synthesize "is_trans_apply_image" from_definition assuming "nonempty"
arity_theorem for "is_trans_apply_image_fm"


definition transrec_apply_image_body where
  "transrec_apply_image_body(M,f,mesa,x,z)   y[M]. pair(M, x, y, z) 
                                (fa[M].
                                    (z[M].
                                        z  fa 
                                        (xa[M].
                                            y[M].
                                               xaa[M].
                                                  sx[M].
                                                     r_sx[M].
                                                        f_r_sx[M].
                                                           pair(M, xa, y, z) 
                                                           pair(M, xa, x, xaa) 
                                                           upair(M, xa, xa, sx) 
                                                           pre_image(M, mesa, sx, r_sx) 
                                                           restriction(M, fa, r_sx, f_r_sx) 
                                                           xaa  mesa  is_trans_apply_image(M, f, xa, f_r_sx, y))) 
                                    is_trans_apply_image(M, f, x, fa, y))"

synthesize "transrec_apply_image_body" from_definition assuming "nonempty"
arity_theorem for "transrec_apply_image_body_fm"

 definition is_trans_apply_image_body where
  "is_trans_apply_image_body(M,f,β,a,w)  z[M]. pair(M,a,z,w)  aβ  (sa[M].
                 esa[M].
                    mesa[M].
                      upair(M, a, a, sa) 
                       is_eclose(M, sa, esa) 
                      membership(M, esa, mesa) 
                      (fa[M].
                          (z[M].
                              z  fa 
                              (x[M].
                                  y[M].
                                     xa[M].
                                        sx[M].
                                           r_sx[M].
                                              f_r_sx[M].
                                                 pair(M, x, y, z) 
                                                 pair(M, x, a, xa) 
                                                 upair(M, x, x, sx) 
                                                 pre_image(M, mesa, sx, r_sx) 
                                                 restriction(M, fa, r_sx, f_r_sx) 
                                                 xa  mesa  is_trans_apply_image(M, f, x, f_r_sx, y))) 
                          is_trans_apply_image(M, f, a, fa, z)))"


synthesize "is_trans_apply_image_body" from_definition assuming "nonempty"
arity_theorem for "is_trans_apply_image_body_fm"

definition replacement_is_omega_funspace_fm where "replacement_is_omega_funspace_fm   omega_funspace_fm(2,0,1)"
definition wfrec_Aleph_fm where "wfrec_Aleph_fm   HAleph_wfrec_repl_body_fm(2,0,1)"
definition replacement_is_fst2_snd2_fm where "replacement_is_fst2_snd2_fm   is_fst2_snd2_fm(0,1)"
definition replacement_is_sndfst_fst2_snd2_fm where "replacement_is_sndfst_fst2_snd2_fm   is_sndfst_fst2_snd2_fm(0,1)"
definition omap_replacement_fm where "omap_replacement_fm   order_eq_map_fm(2,3,0,1)"
definition rec_constr_abs_fm where "rec_constr_abs_fm   transrec_apply_image_body_fm(3,2,0,1)"
definition banach_replacement_iterates_fm where "banach_replacement_iterates_fm  banach_is_iterates_body_fm(6,5,4,3,2,0,1)"
definition rec_constr_fm where "rec_constr_fm  is_trans_apply_image_body_fm(3,2,0,1)"
(* definition banach_iterates_fm where "banach_iterates_fm ≡ banach_body_iterates_fm(7,6,5,4,3,2,0,1)" *)
definition dc_abs_fm where "dc_abs_fm  dcwit_repl_body_fm(6,5,4,3,2,0,1)"
definition lam_replacement_check_fm where "lam_replacement_check_fm  Lambda_in_M_fm(check_fm(2,0,1),1)"

text‹The following instances are needed only on the ground model. The
first one corresponds to the recursive definition of forces for atomic
formulas; the next two corresponds to termPHcheck; the following
is used to get a generic filter using some form of choice.›

locale M_ZF_ground = M_ZF1 +
  assumes
    ZF_ground_replacements:
    "replacement_assm(M,env,wfrec_Hfrc_at_fm)"
    "replacement_assm(M,env,wfrec_Hcheck_fm)"
    "replacement_assm(M,env,lam_replacement_check_fm)"

locale M_ZF_ground_trans = M_ZF1_trans + M_ZF_ground

definition instances_ground_fms where "instances_ground_fms 
  { wfrec_Hfrc_at_fm,
    wfrec_Hcheck_fm,
    lam_replacement_check_fm }"

lemmas replacement_instances_ground_defs =
  wfrec_Hfrc_at_fm_def wfrec_Hcheck_fm_def lam_replacement_check_fm_def

declare (in M_ZF_ground) replacement_instances_ground_defs [simp]

lemma instances_ground_fms_type[TC]: "instances_ground_fms  formula"
  using Lambda_in_M_fm_type
  unfolding instances_ground_fms_def replacement_instances_ground_defs
  by simp

locale M_ZF_ground_notCH = M_ZF_ground +
  assumes
    ZF_ground_notCH_replacements:
    "replacement_assm(M,env,rec_constr_abs_fm)"
    "replacement_assm(M,env,rec_constr_fm)"

definition instances_ground_notCH_fms where "instances_ground_notCH_fms 
  { rec_constr_abs_fm,
    rec_constr_fm }"

lemma instances_ground_notCH_fms_type[TC]: "instances_ground_notCH_fms  formula"
  unfolding instances_ground_notCH_fms_def rec_constr_abs_fm_def
    rec_constr_fm_def
  by simp

declare (in M_ZF_ground_notCH) rec_constr_abs_fm_def[simp]
  rec_constr_fm_def[simp]

locale M_ZF_ground_notCH_trans = M_ZF_ground_trans + M_ZF_ground_notCH

locale M_ZF_ground_CH = M_ZF_ground_notCH +
  assumes
    dcwit_replacement: "replacement_assm(M,env,dc_abs_fm)"

declare (in M_ZF_ground_CH) dc_abs_fm_def [simp]

locale M_ZF_ground_CH_trans = M_ZF_ground_notCH_trans + M_ZF_ground_CH

locale M_ctm1 = M_ZF1_trans + M_ZF_ground_trans +
  fixes enum
  assumes M_countable:      "enumbij(nat,M)"

locale M_ctm1_AC = M_ctm1 + M_ZFC1_trans

context M_ZF_ground_CH_trans
begin

lemma replacement_dcwit_repl_body:
  "(##M)(mesa)  (##M)(A)  (##M)(a)  (##M)(s)  (##M)(R) 
   strong_replacement(##M, dcwit_repl_body(##M,mesa,A,a,s,R))"
  using strong_replacement_rel_in_ctm[where φ="dcwit_repl_body_fm(6,5,4,3,2,0,1)"
      and env="[R,s,a,A,mesa]" and f="dcwit_repl_body(##M,mesa,A,a,s,R)"]
    zero_in_M arity_dcwit_repl_body dcwit_replacement
  unfolding dc_abs_fm_def
  by simp

lemma dcwit_repl:
  "(##M)(sa) 
        (##M)(esa) 
        (##M)(mesa)  (##M)(A)  (##M)(a)  (##M)(s)  (##M)(R) 
        strong_replacement
              ((##M), λx z. y[(##M)]. pair((##M), x, y, z) 
                                is_wfrec
                                 ((##M), λn f. is_nat_case
                                             ((##M), a,
                                              λm bmfm.
                                                 fm[(##M)].
                                                    cp[(##M)].
                                                       is_apply((##M), f, m, fm) 
                                                       is_Collect((##M), A, λx. fmx[(##M)]. ((##M)(x)  fmx  R)  pair((##M), fm, x, fmx), cp) 
                                                       is_apply((##M), s, cp, bmfm),
                                              n),
                                  mesa, x, y))"
  using replacement_dcwit_repl_body unfolding dcwit_repl_body_def by simp

end ― ‹localeM_ZF_ground_CH_trans

context M_ZF1_trans
begin

lemmas M_replacement_ZF_instances = lam_replacement_fst lam_replacement_snd
  lam_replacement_Union lam_replacement_Image
  lam_replacement_middle_del lam_replacement_prodRepl

lemmas M_separation_ZF_instances = separation_fstsnd_in_sndsnd separation_sndfst_eq_fstsnd

lemma separation_is_dcwit_body:
  assumes "(##M)(A)" "(##M)(a)" "(##M)(g)" "(##M)(R)"
  shows "separation(##M,is_dcwit_body(##M, A, a, g, R))"
  using assms separation_in_ctm[where env="[A,a,g,R]" and φ="is_dcwit_body_fm(1,2,3,4,0)",
      OF _ _ _ is_dcwit_body_iff_sats[symmetric],
      of "λ_.A" "λ_.a" "λ_.g" "λ_.R" "λx. x"]
    nonempty arity_is_dcwit_body_fm is_dcwit_body_fm_type
  by (simp add:ord_simp_union)

end ― ‹localeM_ZF1_trans

sublocale M_ZF1_trans  M_replacement "##M"
  using M_replacement_ZF_instances M_separation_ZF_instances
  by unfold_locales simp

context M_ZF1_trans
begin

lemma separation_Pow_rel: "AM 
    separation(##M, λy. x  M . xA  y = x, Pow⇗##M⇖(x))"
  using separation_assm_sats[of "is_Pow_fm(0,1)"] arity_is_Pow_fm ord_simp_union
    Pow_rel_closed nonempty Pow_rel_iff
  by simp

lemma strong_replacement_Powapply_rel:
  "fM  strong_replacement(##M, λx y. y = Powapply⇗##M⇖(f,x))"
  using Powapply_rel_replacement separation_Pow_rel transM
  by simp

end ― ‹localeM_ZF1_trans

sublocale M_ZF1_trans  M_Vfrom "##M"
  using power_ax strong_replacement_Powapply_rel phrank_repl trans_repl_HVFrom wfrec_rank
  by unfold_locales auto

sublocale M_ZF1_trans  M_Perm "##M"
  using separation_PiP_rel separation_injP_rel separation_surjP_rel
    lam_replacement_imp_strong_replacement[OF
      lam_replacement_Sigfun[OF lam_replacement_constant]]
    Pi_replacement1 unfolding Sigfun_def
  by unfold_locales simp_all

sublocale M_ZF1_trans  M_pre_seqspace "##M"
  by unfold_locales

context M_ZF1_trans
begin

lemma separation_inj_rel: "AM 
     separation(##M, λy. xM. x  A  y = x, inj_rel(##M,fst(x), snd(x)))"
  using arity_is_inj_fm ord_simp_union
    nonempty inj_rel_closed[simplified] inj_rel_iff[simplified]
  by (rule_tac separation_assm_bin_sats[of "is_inj_fm(0,1,2)"])
    (simp_all add:setclass_def)

lemma lam_replacement_inj_rel: "lam_replacement(##M, λx . inj_rel(##M,fst(x),snd(x)))"
  using lam_replacement_inj_rel' separation_inj_rel
  by simp

(*

These lemmas were required for the original proof of Schröder-Bernstein.

lemma banach_iterates:
  assumes "X∈M" "Y∈M" "f∈M" "g∈M" "W∈M"
  shows "iterates_replacement(##M, is_banach_functor(##M,X,Y,f,g), W)"
proof -
  have "strong_replacement(##M, λ x z . banach_body_iterates(##M,X,Y,f,g,W,n,x,z))" if "n∈ω" for n
    using assms that arity_banach_body_iterates_fm ord_simp_union nat_into_M
      strong_replacement_rel_in_ctm[where φ="banach_body_iterates_fm(7,6,5,4,3,2,0,1)"
        and env="[n,W,g,f,Y,X]"] replacement_ax2(3)
    by simp
  then
  show ?thesis
    using assms nat_into_M Memrel_closed
    unfolding iterates_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def
      is_nat_case_def iterates_MH_def banach_body_iterates_def
    by simp
qed

lemma separation_banach_functor_iterates:
  assumes "X∈M" "Y∈M" "f∈M" "g∈M" "A∈M"
  shows "separation(##M, λb. ∃x∈A. x ∈ ω ∧ b = banach_functor(X, Y, f, g)^x (0))"
proof -
  have " (∃xa∈M. xa ∈ A ∧ xa ∈ ω ∧ banach_is_iterates_body(##M, X, Y, f, g, 0, xa, x)) ⟷
         (∃n∈A. n ∈ ω ∧ banach_is_iterates_body(##M, X, Y, f, g, 0, n, x))" if "x∈M" for x
    using assms nat_into_M nat_in_M transM[of _ A] transM[of _ ω] that
    by auto
  then
  have "separation(##M, λ z . ∃n∈A . n∈ω ∧ banach_is_iterates_body(##M,X,Y,f,g,0,n,z))"
    using assms nat_into_M nat_in_M
      arity_banach_is_iterates_body_fm[of 6 5 4 3 2 0 1] ord_simp_union
      separation_in_ctm[where φ="(⋅∃ ⋅⋅0∈7⋅ ∧ ⋅⋅0∈8⋅ ∧ banach_is_iterates_body_fm(6,5,4,3,2,0,1) ⋅⋅⋅)"
        and env="[0,g,f,Y,X,A,ω]"]
    by (simp add:arity_Exists arity_And)
  moreover from assms
  have "(∃x∈A. x ∈ ω ∧ is_iterates(##M,is_banach_functor(##M,X, Y, f, g),0,x,z)) ⟷
          (∃n∈A . n∈ω ∧ banach_is_iterates_body(##M,X,Y,f,g,0,n,z))" if "z∈M" for z
    using nat_in_M nat_into_M transM[of _ A] transM[of _ ω]
    unfolding is_iterates_def wfrec_replacement_def is_wfrec_def M_is_recfun_def
      is_nat_case_def iterates_MH_def banach_body_iterates_def banach_is_iterates_body_def
    by simp
  moreover from assms
  have "(∃x∈A. x ∈ ω ∧ is_iterates(##M,is_banach_functor(##M,X, Y, f, g),0,x,z)) ⟷
          (∃x∈A. x ∈ ω ∧ z = banach_functor(X, Y, f, g)^x (0))" if "z∈M" for z
    using transM[of _ A] nat_in_M nat_into_M that
      iterates_abs[OF banach_iterates banach_functor_abs] banach_functor_closed
    by auto
  ultimately
  show ?thesis
    by(rule_tac separation_cong[THEN iffD2],auto)
qed

lemma banach_replacement:
  assumes "X∈M" "Y∈M" "f∈M" "g∈M"
  shows "strong_replacement(##M, λn y. n∈nat ∧ y = banach_functor(X, Y, f, g)^n (0))"
  using assms banach_repl_iter' separation_banach_functor_iterates
  by simp

*)

end ― ‹localeM_ZF1_trans

lemma (in M_basic) rel2_trans_apply:
  "M(f)  relation2(M,is_trans_apply_image(M,f),trans_apply_image(f))"
  unfolding is_trans_apply_image_def trans_apply_image_def relation2_def
  by auto

lemma (in M_basic) apply_image_closed:
  shows "M(f)  x[M]. g[M]. M(trans_apply_image(f, x, g))"
  unfolding trans_apply_image_def by simp

context M_ZF_ground_notCH_trans
begin

lemma replacement_transrec_apply_image_body :
  "(##M)(f)  (##M)(mesa)  strong_replacement(##M,transrec_apply_image_body(##M,f,mesa))"
  using strong_replacement_rel_in_ctm[where φ="transrec_apply_image_body_fm(3,2,0,1)" and env="[mesa,f]"]
    zero_in_M arity_transrec_apply_image_body_fm ord_simp_union
    ZF_ground_notCH_replacements(1)
  by simp

lemma transrec_replacement_apply_image:
  assumes "(##M)(f)" "(##M)(α)"
  shows "transrec_replacement(##M, is_trans_apply_image(##M, f), α)"
  using replacement_transrec_apply_image_body[unfolded transrec_apply_image_body_def] assms
    Memrel_closed singleton_closed eclose_closed
  unfolding transrec_replacement_def wfrec_replacement_def is_wfrec_def M_is_recfun_def
  by simp

lemma rec_trans_apply_image_abs:
  assumes "(##M)(f)" "(##M)(x)" "(##M)(y)" "Ord(x)"
  shows "is_transrec(##M,is_trans_apply_image(##M, f),x,y)  y = transrec(x,trans_apply_image(f))"
  using transrec_abs[OF transrec_replacement_apply_image rel2_trans_apply] assms apply_image_closed
  by simp

lemma replacement_is_trans_apply_image:
  "(##M)(f)  (##M)(β)  strong_replacement(##M, λ x z .
    y[##M]. pair(##M,x,y,z)  xβ  (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))"
  unfolding is_transrec_def is_wfrec_def M_is_recfun_def
  apply(rule_tac strong_replacement_cong[
        where P="λ x z. M,[x,z,β,f]  is_trans_apply_image_body_fm(3,2,0,1)",THEN iffD1])
   apply(rule_tac is_trans_apply_image_body_iff_sats[symmetric,unfolded is_trans_apply_image_body_def,where env="[_,_,β,f]"])
            apply(simp_all add:zero_in_M)
  apply(rule_tac ZF_ground_notCH_replacements(2)[unfolded replacement_assm_def, rule_format, where env="[β,f]",simplified])
    apply(simp_all add: arity_is_trans_apply_image_body_fm is_trans_apply_image_body_fm_type ord_simp_union)
  done

lemma trans_apply_abs:
  "(##M)(f)  (##M)(β)  Ord(β)  (##M)(x)  (##M)(z) 
    (xβ  z = x, transrec(x, λa g. f ` (g `` a)) ) 
    (y[##M]. pair(##M,x,y,z)  xβ  (is_transrec(##M,is_trans_apply_image(##M, f),x,y)))"
  using rec_trans_apply_image_abs Ord_in_Ord
    transrec_closed[OF transrec_replacement_apply_image rel2_trans_apply,of f,simplified]
    apply_image_closed
  unfolding trans_apply_image_def
  by auto

lemma replacement_trans_apply_image:
  "(##M)(f)  (##M)(β)  Ord(β) 
  strong_replacement(##M, λx y. xβ  y = x, transrec(x, λa g. f ` (g `` a)))"
  using strong_replacement_cong[THEN iffD1,OF _ replacement_is_trans_apply_image,simplified]
    trans_apply_abs Ord_in_Ord
  by simp

end ― ‹localeM_ZF_ground_notCH_trans

definition ifrFb_body where
  "ifrFb_body(M,b,f,x,i)  x 
  (if b = 0 then if i  range(f) then
  if M(converse(f) ` i) then converse(f) ` i else 0 else 0 else if M(i) then i else 0)"

relativize functional "ifrFb_body" "ifrFb_body_rel"
relationalize "ifrFb_body_rel" "is_ifrFb_body"

synthesize "is_ifrFb_body" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body_fm"

definition ifrangeF_body :: "[io,i,i,i,i]  o" where
  "ifrangeF_body(M,A,b,f)  λy. xA. y = x,μ i. ifrFb_body(M,b,f,x,i)"

relativize functional "ifrangeF_body" "ifrangeF_body_rel"
relationalize "ifrangeF_body_rel" "is_ifrangeF_body"

synthesize "is_ifrangeF_body" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body_fm"

lemma (in M_Z_trans) separation_is_ifrangeF_body:
  "(##M)(A)  (##M)(r)  (##M)(s)  separation(##M, is_ifrangeF_body(##M,A,r,s))"
  using separation_in_ctm[where φ="is_ifrangeF_body_fm(1,2,3,0)" and env="[A,r,s]"]
    zero_in_M arity_is_ifrangeF_body_fm ord_simp_union is_ifrangeF_body_fm_type
  by simp

lemma (in M_basic) is_ifrFb_body_closed: "M(r)  M(s)  is_ifrFb_body(M, r, s, x, i)  M(i)"
  unfolding ifrangeF_body_def is_ifrangeF_body_def is_ifrFb_body_def If_abs
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF1_trans) ifrangeF_body_abs:
  assumes "(##M)(A)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ifrangeF_body(##M,A,r,s,x)  ifrangeF_body(##M,A,r,s,x)"
proof -
  {
    fix a
    assume "aM"
    with assms
    have "(μ i. i M  is_ifrFb_body(##M, r, s, z, i))= (μ i. is_ifrFb_body(##M, r, s, z, i))" for z
      using is_ifrFb_body_closed[of r s z]
      by (rule_tac Least_cong[of "λi. iM  is_ifrFb_body(##M,r,s,z,i)"]) auto
    moreover
    have "(μ i. is_ifrFb_body(##M, r, s, z, i))= (μ i. ifrFb_body(##M, r, s, z, i))" for z
    proof (rule_tac Least_cong[of "λi. is_ifrFb_body(##M,r,s,z,i)" "λi. ifrFb_body(##M,r,s,z,i)"])
      fix y
      from assms aM
      show "is_ifrFb_body(##M, r, s, z, y)  ifrFb_body(##M, r, s, z, y)"
        using If_abs apply_0
        unfolding ifrFb_body_def is_ifrFb_body_def
        by (cases "yM"; cases "yrange(s)"; cases "converse(s)`y  M";
            auto dest:transM split del: split_if del:iffI)
          (auto simp flip:setclass_iff; (force simp only:setclass_iff))+
    qed
    moreover from aM
    have "least(##M, λi. i  M  is_ifrFb_body(##M, r, s, z, i), a)
       a = (μ i.  i M  is_ifrFb_body(##M, r, s, z,i))" for z
      using If_abs least_abs'[of "λi. (##M)(i)  is_ifrFb_body(##M,r,s,z,i)" a]
      by simp
    ultimately
    have "least(##M, λi. i  M  is_ifrFb_body(##M, r, s, z, i), a)
       a = (μ i. ifrFb_body(##M, r, s, z,i))" for z
      by simp
  }
  with assms
  show ?thesis
    using  pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
    unfolding ifrangeF_body_def is_ifrangeF_body_def
    by (auto dest:transM)
qed

lemma (in M_ZF1_trans) separation_ifrangeF_body:
  "(##M)(A)  (##M)(b)  (##M)(f)  separation
        (##M, λy.  xA. y = x, μ i. x  if_range_F_else_F(λx. if (##M)(x) then x else 0, b, f, i))"
  using separation_is_ifrangeF_body ifrangeF_body_abs
    separation_cong[where P="is_ifrangeF_body(##M,A,b,f)" and M="##M",THEN iffD1]
  unfolding ifrangeF_body_def if_range_F_def if_range_F_else_F_def ifrFb_body_def
  by simp

(* (##M)(A) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
    separation(##M,
      λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. if (##M)(a) then G`a else 0, b, f, i)⟩) *)

definition ifrFb_body2 where
  "ifrFb_body2(M,G,b,f,x,i)  x 
  (if b = 0 then if i  range(f) then
  if M(converse(f) ` i) then G`(converse(f) ` i) else 0 else 0 else if M(i) then G`i else 0)"

relativize functional "ifrFb_body2" "ifrFb_body2_rel"
relationalize "ifrFb_body2_rel" "is_ifrFb_body2"

synthesize "is_ifrFb_body2" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body2_fm"

definition ifrangeF_body2 :: "[io,i,i,i,i,i]  o" where
  "ifrangeF_body2(M,A,G,b,f)  λy. xA. y = x,μ i. ifrFb_body2(M,G,b,f,x,i)"

relativize functional "ifrangeF_body2" "ifrangeF_body2_rel"
relationalize "ifrangeF_body2_rel" "is_ifrangeF_body2"

synthesize "is_ifrangeF_body2" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body2_fm"

lemma (in M_Z_trans) separation_is_ifrangeF_body2:
  "(##M)(A)  (##M)(G)  (##M)(r)  (##M)(s)  separation(##M, is_ifrangeF_body2(##M,A,G,r,s))"
  using separation_in_ctm[where φ="is_ifrangeF_body2_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
    zero_in_M arity_is_ifrangeF_body2_fm ord_simp_union is_ifrangeF_body2_fm_type
  by simp

lemma (in M_basic) is_ifrFb_body2_closed: "M(G)  M(r)  M(s)  is_ifrFb_body2(M, G, r, s, x, i)  M(i)"
  unfolding ifrangeF_body2_def is_ifrangeF_body2_def is_ifrFb_body2_def If_abs
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF1_trans) ifrangeF_body2_abs:
  assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ifrangeF_body2(##M,A,G,r,s,x)  ifrangeF_body2(##M,A,G,r,s,x)"
proof -
  {
    fix a
    assume "aM"
    with assms
    have "(μ i. i M  is_ifrFb_body2(##M, G, r, s, z, i))= (μ i. is_ifrFb_body2(##M, G, r, s, z, i))" for z
      using is_ifrFb_body2_closed[of G r s z]
      by (rule_tac Least_cong[of "λi. iM  is_ifrFb_body2(##M,G,r,s,z,i)"]) auto
    moreover
    have "(μ i. is_ifrFb_body2(##M, G, r, s, z, i))= (μ i. ifrFb_body2(##M, G, r, s, z, i))" for z
    proof (rule_tac Least_cong[of "λi. is_ifrFb_body2(##M,G,r,s,z,i)" "λi. ifrFb_body2(##M,G,r,s,z,i)"])
      fix y
      from assms aM
      show "is_ifrFb_body2(##M, G, r, s, z, y)  ifrFb_body2(##M, G, r, s, z, y)"
        using If_abs apply_0
        unfolding ifrFb_body2_def is_ifrFb_body2_def
        by (cases "yM"; cases "yrange(s)"; cases "converse(s)`y  M";
            auto dest:transM split del: split_if del:iffI)
          (auto simp flip:setclass_iff; (force simp only:setclass_iff))+
    qed
    moreover from aM
    have "least(##M, λi. i  M  is_ifrFb_body2(##M, G, r, s, z, i), a)
       a = (μ i.  i M  is_ifrFb_body2(##M, G, r, s, z,i))" for z
      using If_abs least_abs'[of "λi. (##M)(i)  is_ifrFb_body2(##M,G,r,s,z,i)" a]
      by simp
    ultimately
    have "least(##M, λi. i  M  is_ifrFb_body2(##M, G, r, s, z, i), a)
       a = (μ i. ifrFb_body2(##M, G, r, s, z,i))" for z
      by simp
  }
  with assms
  show ?thesis
    using  pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
    unfolding ifrangeF_body2_def is_ifrangeF_body2_def
    by (auto dest:transM)
qed

lemma (in M_ZF1_trans) separation_ifrangeF_body2:
  "(##M)(A)  (##M)(G)  (##M)(b)  (##M)(f) 
       separation
        (##M,
         λy. xA.
                y =
                x, μ i. x 
                         if_range_F_else_F(λa. if (##M)(a) then G ` a else 0, b, f, i))"
  using separation_is_ifrangeF_body2 ifrangeF_body2_abs
    separation_cong[where P="is_ifrangeF_body2(##M,A,G,b,f)" and M="##M",THEN iffD1]
  unfolding ifrangeF_body2_def if_range_F_def if_range_F_else_F_def ifrFb_body2_def
  by simp

(* (##M)(A) ⟹ (##M)(b) ⟹ (##M)(f) ⟹ (##M)(F) ⟹
  separation(##M,
    λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. if (##M)(a) then F -`` {a} else 0, b, f, i)⟩) *)

definition ifrFb_body3 where
  "ifrFb_body3(M,G,b,f,x,i)  x 
  (if b = 0 then if i  range(f) then
  if M(converse(f) ` i) then G-``{converse(f) ` i} else 0 else 0 else if M(i) then G-``{i} else 0)"

relativize functional "ifrFb_body3" "ifrFb_body3_rel"
relationalize "ifrFb_body3_rel" "is_ifrFb_body3"

synthesize "is_ifrFb_body3" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body3_fm"

definition ifrangeF_body3 :: "[io,i,i,i,i,i]  o" where
  "ifrangeF_body3(M,A,G,b,f)  λy. xA. y = x,μ i. ifrFb_body3(M,G,b,f,x,i)"

relativize functional "ifrangeF_body3" "ifrangeF_body3_rel"
relationalize "ifrangeF_body3_rel" "is_ifrangeF_body3"

synthesize "is_ifrangeF_body3" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body3_fm"

lemma (in M_Z_trans) separation_is_ifrangeF_body3:
  "(##M)(A)  (##M)(G)  (##M)(r)  (##M)(s)  separation(##M, is_ifrangeF_body3(##M,A,G,r,s))"
  using separation_in_ctm[where φ="is_ifrangeF_body3_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
    zero_in_M arity_is_ifrangeF_body3_fm ord_simp_union is_ifrangeF_body3_fm_type
  by simp

lemma (in M_basic) is_ifrFb_body3_closed: "M(G)  M(r)  M(s)  is_ifrFb_body3(M, G, r, s, x, i)  M(i)"
  unfolding ifrangeF_body3_def is_ifrangeF_body3_def is_ifrFb_body3_def If_abs
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF1_trans) ifrangeF_body3_abs:
  assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ifrangeF_body3(##M,A,G,r,s,x)  ifrangeF_body3(##M,A,G,r,s,x)"
proof -
  {
    fix a
    assume "aM"
    with assms
    have "(μ i. i M  is_ifrFb_body3(##M, G, r, s, z, i))= (μ i. is_ifrFb_body3(##M, G, r, s, z, i))" for z
      using is_ifrFb_body3_closed[of G r s z]
      by (rule_tac Least_cong[of "λi. iM  is_ifrFb_body3(##M,G,r,s,z,i)"]) auto
    moreover
    have "(μ i. is_ifrFb_body3(##M, G, r, s, z, i))= (μ i. ifrFb_body3(##M, G, r, s, z, i))" for z
    proof (rule_tac Least_cong[of "λi. is_ifrFb_body3(##M,G,r,s,z,i)" "λi. ifrFb_body3(##M,G,r,s,z,i)"])
      fix y
      from assms aM
      show "is_ifrFb_body3(##M, G, r, s, z, y)  ifrFb_body3(##M, G, r, s, z, y)"
        using If_abs apply_0
        unfolding ifrFb_body3_def is_ifrFb_body3_def
        by (cases "yM"; cases "yrange(s)"; cases "converse(s)`y  M";
            auto dest:transM split del: split_if del:iffI)
          (auto simp flip:setclass_iff; (force simp only:setclass_iff))+
    qed
    moreover from aM
    have "least(##M, λi. i  M  is_ifrFb_body3(##M, G, r, s, z, i), a)
       a = (μ i.  i M  is_ifrFb_body3(##M, G, r, s, z,i))" for z
      using If_abs least_abs'[of "λi. (##M)(i)  is_ifrFb_body3(##M,G,r,s,z,i)" a]
      by simp
    ultimately
    have "least(##M, λi. i  M  is_ifrFb_body3(##M, G, r, s, z, i), a)
       a = (μ i. ifrFb_body3(##M, G, r, s, z,i))" for z
      by simp
  }
  with assms
  show ?thesis
    using  pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
    unfolding ifrangeF_body3_def is_ifrangeF_body3_def
    by (auto dest:transM)
qed

lemma (in M_ZF1_trans) separation_ifrangeF_body3:
  "(##M)(A)  (##M)(G)  (##M)(b)  (##M)(f) 
       separation
        (##M,
         λy. xA.
                y =
                x, μ i. x 
                         if_range_F_else_F(λa. if (##M)(a) then G-``{a} else 0, b, f, i))"
  using separation_is_ifrangeF_body3 ifrangeF_body3_abs
    separation_cong[where P="is_ifrangeF_body3(##M,A,G,b,f)" and M="##M",THEN iffD1]
  unfolding ifrangeF_body3_def if_range_F_def if_range_F_else_F_def ifrFb_body3_def
  by simp

(* (##M)(A) ⟹ (##M)(b) ⟹ (##M)(f) ⟹ (##M)(A') ⟹
    separation(##M, λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F((`)(A), b, f, i)⟩) *)

definition ifrFb_body4 where
  "ifrFb_body4(G,b,f,x,i)  x 
  (if b = 0 then if i  range(f) then G`(converse(f) ` i) else 0 else G`i)"

relativize functional "ifrFb_body4" "ifrFb_body4_rel"
relationalize "ifrFb_body4_rel" "is_ifrFb_body4"

synthesize "is_ifrFb_body4" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body4_fm"

definition ifrangeF_body4 :: "[io,i,i,i,i,i]  o" where
  "ifrangeF_body4(M,A,G,b,f)  λy. xA. y = x,μ i. ifrFb_body4(G,b,f,x,i)"

relativize functional "ifrangeF_body4" "ifrangeF_body4_rel"
relationalize "ifrangeF_body4_rel" "is_ifrangeF_body4"

synthesize "is_ifrangeF_body4" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body4_fm"

lemma (in M_Z_trans) separation_is_ifrangeF_body4:
  "(##M)(A)  (##M)(G)  (##M)(r)  (##M)(s)  separation(##M, is_ifrangeF_body4(##M,A,G,r,s))"
  using separation_in_ctm[where φ="is_ifrangeF_body4_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
    zero_in_M arity_is_ifrangeF_body4_fm ord_simp_union is_ifrangeF_body4_fm_type
  by simp

lemma (in M_basic) is_ifrFb_body4_closed: "M(G)  M(r)  M(s)  is_ifrFb_body4(M, G, r, s, x, i)  M(i)"
  using If_abs
  unfolding ifrangeF_body4_def is_ifrangeF_body4_def is_ifrFb_body4_def fun_apply_def
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF1_trans) ifrangeF_body4_abs:
  assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ifrangeF_body4(##M,A,G,r,s,x)  ifrangeF_body4(##M,A,G,r,s,x)"
proof -
  {
    fix a
    assume "aM"
    with assms
    have "(μ i. i M  is_ifrFb_body4(##M, G, r, s, z, i))= (μ i. is_ifrFb_body4(##M, G, r, s, z, i))" for z
      using is_ifrFb_body4_closed[of G r s z]
      by (rule_tac Least_cong[of "λi. iM  is_ifrFb_body4(##M,G,r,s,z,i)"]) auto
    moreover
    have "(μ i. is_ifrFb_body4(##M, G, r, s, z, i))= (μ i. ifrFb_body4(G, r, s, z, i))" if "zM" for z
    proof (rule_tac Least_cong[of "λi. is_ifrFb_body4(##M,G,r,s,z,i)" "λi. ifrFb_body4(G,r,s,z,i)"])
      fix y
      from assms aM zM
      show "is_ifrFb_body4(##M, G, r, s, z, y)  ifrFb_body4(G, r, s, z, y)"
        using If_abs apply_0
        unfolding ifrFb_body4_def is_ifrFb_body4_def
        apply (cases "yM"; cases "yrange(s)"; cases "r=0"; cases "ydomain(G)";
            auto dest:transM split del: split_if del:iffI)
        by (auto simp flip:setclass_iff; (force simp only: fun_apply_def setclass_iff))
          (auto simp flip:setclass_iff simp: fun_apply_def )
    qed
    moreover from aM
    have "least(##M, λi. i  M  is_ifrFb_body4(##M, G, r, s, z, i), a)
       a = (μ i.  i M  is_ifrFb_body4(##M, G, r, s, z,i))" for z
      using If_abs least_abs'[of "λi. (##M)(i)  is_ifrFb_body4(##M,G,r,s,z,i)" a]
      by simp
    ultimately
    have "zM  least(##M, λi. i  M  is_ifrFb_body4(##M, G, r, s, z, i), a)
       a = (μ i. ifrFb_body4(G, r, s, z,i))" for z
      by simp
  }
  with assms
  show ?thesis
    using  pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
    unfolding ifrangeF_body4_def is_ifrangeF_body4_def
    by (auto dest:transM)
qed

lemma (in M_ZF1_trans) separation_ifrangeF_body4:
  "(##M)(A)  (##M)(G)  (##M)(b)  (##M)(f) 
       separation(##M, λy. xA. y = x, μ i. x  if_range_F_else_F((`)(G), b, f, i))"
  using separation_is_ifrangeF_body4 ifrangeF_body4_abs
    separation_cong[where P="is_ifrangeF_body4(##M,A,G,b,f)" and M="##M",THEN iffD1]
  unfolding ifrangeF_body4_def if_range_F_def if_range_F_else_F_def ifrFb_body4_def
  by simp

(* (##M)(G) ⟹ (##M)(A) ⟹
    separation(##M,
      λy. ∃x∈A. y = ⟨x, μ i. x ∈ if_range_F_else_F(λx. {xa ∈ G . x ∈ xa}, b, f, i)⟩) *)

definition ifrFb_body5 where
  "ifrFb_body5(G,b,f,x,i)  x 
  (if b = 0 then if i  range(f) then {xa  G . converse(f) ` i  xa} else 0 else {xa  G . i  xa})"

relativize functional "ifrFb_body5" "ifrFb_body5_rel"
relationalize "ifrFb_body5_rel" "is_ifrFb_body5"

synthesize "is_ifrFb_body5" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body5_fm"

definition ifrangeF_body5 :: "[io,i,i,i,i,i]  o" where
  "ifrangeF_body5(M,A,G,b,f)  λy. xA. y = x,μ i. ifrFb_body5(G,b,f,x,i)"

relativize functional "ifrangeF_body5" "ifrangeF_body5_rel"
relationalize "ifrangeF_body5_rel" "is_ifrangeF_body5"

synthesize "is_ifrangeF_body5" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body5_fm"

lemma (in M_Z_trans) separation_is_ifrangeF_body5:
  "(##M)(A)  (##M)(G)  (##M)(r)  (##M)(s)  separation(##M, is_ifrangeF_body5(##M,A,G,r,s))"
  using separation_in_ctm[where φ="is_ifrangeF_body5_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
    zero_in_M arity_is_ifrangeF_body5_fm ord_simp_union is_ifrangeF_body5_fm_type
  by simp

lemma (in M_basic) is_ifrFb_body5_closed: "M(G)  M(r)  M(s)  is_ifrFb_body5(M, G, r, s, x, i)  M(i)"
  using If_abs
  unfolding ifrangeF_body5_def is_ifrangeF_body5_def is_ifrFb_body5_def fun_apply_def
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF1_trans) ifrangeF_body5_abs:
  assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ifrangeF_body5(##M,A,G,r,s,x)  ifrangeF_body5(##M,A,G,r,s,x)"
proof -
  {
    fix a
    assume "aM"
    with assms
    have "(μ i. i M  is_ifrFb_body5(##M, G, r, s, z, i))= (μ i. is_ifrFb_body5(##M, G, r, s, z, i))" for z
      using is_ifrFb_body5_closed[of G r s z]
      by (rule_tac Least_cong[of "λi. iM  is_ifrFb_body5(##M,G,r,s,z,i)"]) auto
    moreover
    have "(μ i. is_ifrFb_body5(##M, G, r, s, z, i))= (μ i. ifrFb_body5(G, r, s, z, i))" if "zM" for z
    proof (rule_tac Least_cong[of "λi. is_ifrFb_body5(##M,G,r,s,z,i)" "λi. ifrFb_body5(G,r,s,z,i)"])
      fix y
      from assms aM zM
      show "is_ifrFb_body5(##M, G, r, s, z, y)  ifrFb_body5(G, r, s, z, y)"
        using If_abs apply_0 separation_in_constant separation_in_rev
        unfolding ifrFb_body5_def is_ifrFb_body5_def
        apply (cases "yM"; cases "yrange(s)"; cases "r=0"; cases "ydomain(G)";
            auto dest:transM split del: split_if del:iffI)
              apply (auto simp flip:setclass_iff; (force simp only: fun_apply_def setclass_iff))
             apply (auto simp flip:setclass_iff simp: fun_apply_def)
        apply (auto dest:transM)
        done
    qed
    moreover from aM
    have "least(##M, λi. i  M  is_ifrFb_body5(##M, G, r, s, z, i), a)
       a = (μ i.  i M  is_ifrFb_body5(##M, G, r, s, z,i))" for z
      using If_abs least_abs'[of "λi. (##M)(i)  is_ifrFb_body5(##M,G,r,s,z,i)" a]
      by simp
    ultimately
    have "zM  least(##M, λi. i  M  is_ifrFb_body5(##M, G, r, s, z, i), a)
       a = (μ i. ifrFb_body5(G, r, s, z,i))" for z
      by simp
  }
  with assms
  show ?thesis
    using  pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
    unfolding ifrangeF_body5_def is_ifrangeF_body5_def
    by (auto dest:transM)
qed

lemma (in M_ZF1_trans) separation_ifrangeF_body5:
  "(##M)(A)  (##M)(G)  (##M)(b)  (##M)(f) 
       separation(##M, λy. xA. y = x, μ i. x  if_range_F_else_F(λx. {xa  G . x  xa}, b, f, i))"
  using separation_is_ifrangeF_body5 ifrangeF_body5_abs
    separation_cong[where P="is_ifrangeF_body5(##M,A,G,b,f)" and M="##M",THEN iffD1]
  unfolding ifrangeF_body5_def if_range_F_def if_range_F_else_F_def ifrFb_body5_def
  by simp

(* (##M)(A) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
    separation(##M,
      λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(λa. {p ∈ A . domain(p) = a}, b, f, i)⟩) *)

definition ifrFb_body6 where
  "ifrFb_body6(G,b,f,x,i)  x 
  (if b = 0 then if i  range(f) then {pG . domain(p) = converse(f) ` i} else 0 else {pG . domain(p) = i})"

relativize functional "ifrFb_body6" "ifrFb_body6_rel"
relationalize "ifrFb_body6_rel" "is_ifrFb_body6"

synthesize "is_ifrFb_body6" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body6_fm"

definition ifrangeF_body6 :: "[io,i,i,i,i,i]  o" where
  "ifrangeF_body6(M,A,G,b,f)  λy. xA. y = x,μ i. ifrFb_body6(G,b,f,x,i)"

relativize functional "ifrangeF_body6" "ifrangeF_body6_rel"
relationalize "ifrangeF_body6_rel" "is_ifrangeF_body6"

synthesize "is_ifrangeF_body6" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body6_fm"

lemma (in M_Z_trans) separation_is_ifrangeF_body6:
  "(##M)(A)  (##M)(G)  (##M)(r)  (##M)(s)  separation(##M, is_ifrangeF_body6(##M,A,G,r,s))"
  using separation_in_ctm[where φ="is_ifrangeF_body6_fm(1,2,3,4,0)" and env="[A,G,r,s]"]
    zero_in_M arity_is_ifrangeF_body6_fm ord_simp_union is_ifrangeF_body6_fm_type
  by simp

lemma (in M_basic) ifrFb_body6_closed: "M(G)  M(r)  M(s)  ifrFb_body6(G, r, s, x, i)   M(i)  ifrFb_body6(G, r, s, x, i)"
  using If_abs
  unfolding ifrangeF_body6_def is_ifrangeF_body6_def ifrFb_body6_def fun_apply_def
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_basic) is_ifrFb_body6_closed: "M(G)  M(r)  M(s)  is_ifrFb_body6(M, G, r, s, x, i)  M(i)"
  using If_abs
  unfolding ifrangeF_body6_def is_ifrangeF_body6_def is_ifrFb_body6_def fun_apply_def
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF1_trans) ifrangeF_body6_abs:
  assumes "(##M)(A)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ifrangeF_body6(##M,A,G,r,s,x)  ifrangeF_body6(##M,A,G,r,s,x)"
proof -
  {
    fix a
    assume "aM"
    with assms
    have "(μ i. i M  is_ifrFb_body6(##M, G, r, s, z, i))= (μ i. is_ifrFb_body6(##M, G, r, s, z, i))" for z
      using is_ifrFb_body6_closed[of G r s z]
      by (rule_tac Least_cong[of "λi. iM  is_ifrFb_body6(##M,G,r,s,z,i)"]) auto
    moreover
    have "(μ i. iM  is_ifrFb_body6(##M, G, r, s, z, i))= (μ i. iM   ifrFb_body6(G, r, s, z, i))" if "zM" for z
    proof (rule_tac Least_cong[of "λi. iM  is_ifrFb_body6(##M,G,r,s,z,i)" "λi. iM  ifrFb_body6(G,r,s,z,i)"])
      fix y
      from assms aM zM
      show "yM  is_ifrFb_body6(##M, G, r, s, z, y)  yM  ifrFb_body6(G, r, s, z, y)"
        using If_abs apply_0 separation_in_constant transitivity[of _ G]
          separation_closed converse_closed apply_closed range_closed zero_in_M
          separation_cong[OF eq_commute,THEN iffD1,OF domain_eq_separation]
        unfolding ifrFb_body6_def is_ifrFb_body6_def
        by auto
    qed
    moreover from aM
    have "least(##M, λi. i  M  is_ifrFb_body6(##M, G, r, s, z, i), a)
       a = (μ i.  i M  is_ifrFb_body6(##M, G, r, s, z,i))" for z
      using If_abs least_abs'[of "λi. (##M)(i)  is_ifrFb_body6(##M,G,r,s,z,i)" a]
      by simp
    ultimately
    have "zM  least(##M, λi. i  M  is_ifrFb_body6(##M, G, r, s, z, i), a)
       a = (μ i. ifrFb_body6(G, r, s, z,i))" for z
      using Least_cong[OF ifrFb_body6_closed[of G r s]] assms
      by simp
  }
  with assms
  show ?thesis
    using  pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
    unfolding ifrangeF_body6_def is_ifrangeF_body6_def
    by (auto dest:transM)
qed

lemma (in M_ZF1_trans) separation_ifrangeF_body6:
  "(##M)(A)  (##M)(G)  (##M)(b)  (##M)(f) 
       separation(##M,
      λy. xA. y = x, μ i. x  if_range_F_else_F(λa. {p  G . domain(p) = a}, b, f, i))"
  using separation_is_ifrangeF_body6 ifrangeF_body6_abs
    separation_cong[where P="is_ifrangeF_body6(##M,A,G,b,f)" and M="##M",THEN iffD1]
  unfolding ifrangeF_body6_def if_range_F_def if_range_F_else_F_def ifrFb_body6_def
  by simp



(* (##M)(A) ⟹ (##M)(f) ⟹ (##M)(b) ⟹ (##M)(D) ⟹ (##M)(r') ⟹ (##M)(A') ⟹
    separation(##M,
      λy. ∃x∈A'. y = ⟨x, μ i. x ∈ if_range_F_else_F(drSR_Y(r', D, A), b, f, i)⟩) *)

definition ifrFb_body7 where
  "ifrFb_body7(B,D,A,b,f,x,i)  x 
    (if b = 0 then if i  range(f) then
        {d  D . rA. restrict(r, B) = converse(f) ` i  d = domain(r)} else 0
       else {d  D . rA. restrict(r, B) = i  d = domain(r)})"

relativize functional "ifrFb_body7" "ifrFb_body7_rel"
relationalize "ifrFb_body7_rel" "is_ifrFb_body7"

synthesize "is_ifrFb_body7" from_definition assuming "nonempty"
arity_theorem for "is_ifrFb_body7_fm"

definition ifrangeF_body7 :: "[io,i,i,i,i,i,i,i]  o" where
  "ifrangeF_body7(M,A,B,D,G,b,f)  λy. xA. y = x,μ i. ifrFb_body7(B,D,G,b,f,x,i)"

relativize functional "ifrangeF_body7" "ifrangeF_body7_rel"
relationalize "ifrangeF_body7_rel" "is_ifrangeF_body7"

synthesize "is_ifrangeF_body7" from_definition assuming "nonempty"
arity_theorem for "is_ifrangeF_body7_fm"

lemma (in M_Z_trans) separation_is_ifrangeF_body7:
  "(##M)(A)  (##M)(B)  (##M)(D)  (##M)(G)  (##M)(r)  (##M)(s)  separation(##M, is_ifrangeF_body7(##M,A,B,D,G,r,s))"
  using separation_in_ctm[where φ="is_ifrangeF_body7_fm(1,2,3,4,5,6,0)" and env="[A,B,D,G,r,s]"]
    zero_in_M arity_is_ifrangeF_body7_fm ord_simp_union is_ifrangeF_body7_fm_type
  by simp

lemma (in M_basic) ifrFb_body7_closed: "M(B)  M(D)  M(G)  M(r)  M(s) 
  ifrFb_body7(B,D,G, r, s, x, i)   M(i)  ifrFb_body7(B,D,G, r, s, x, i)"
  using If_abs
  unfolding ifrangeF_body7_def is_ifrangeF_body7_def ifrFb_body7_def fun_apply_def
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_basic) is_ifrFb_body7_closed: "M(B)  M(D)  M(G)  M(r)  M(s) 
  is_ifrFb_body7(M, B,D,G, r, s, x, i)  M(i)"
  using If_abs
  unfolding ifrangeF_body7_def is_ifrangeF_body7_def is_ifrFb_body7_def fun_apply_def
  by (cases "irange(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF1_trans) ifrangeF_body7_abs:
  assumes "(##M)(A)"  "(##M)(B)" "(##M)(D)" "(##M)(G)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ifrangeF_body7(##M,A,B,D,G,r,s,x)  ifrangeF_body7(##M,A,B,D,G,r,s,x)"
proof -
  from assms
  have sep_dr: "yM  separation(##M, λd . rM . rG  y = restrict(r, B)  d = domain(r))" for y
    by(rule_tac separation_cong[where P'="λd . r M . rG  y = restrict(r, B)  d = domain(r)",THEN iffD1,OF _
          separation_restrict_eq_dom_eq[rule_format,of G B y]],auto simp:transitivity[of _ G])
  from assms
  have sep_dr'': "yM  separation(##M, λd . rM. r  G  d = domain(r)  converse(s) ` y = restrict(r, B))" for y
    by(rule_tac separation_cong[THEN iffD1,OF _ separation_restrict_eq_dom_eq[rule_format,of G B "converse(s) ` y "]],
        auto simp:transitivity[of _ G] apply_closed[simplified] converse_closed[simplified])
  {
    fix a
    assume "aM"
    with assms
    have "(μ i. i M  is_ifrFb_body7(##M, B,D,G, r, s, z, i))= (μ i. is_ifrFb_body7(##M,B,D, G, r, s, z, i))" for z
      using is_ifrFb_body7_closed[of B D G r s z]
      by (rule_tac Least_cong[of "λi. iM  is_ifrFb_body7(##M,B,D,G,r,s,z,i)"]) auto
    moreover from this
    have "(μ i. iM  is_ifrFb_body7(##M, B,D,G, r, s, z, i))= (μ i. iM   ifrFb_body7(B,D,G, r, s, z, i))" if "zM" for z
    proof (rule_tac Least_cong[of "λi. iM  is_ifrFb_body7(##M,B,D,G,r,s,z,i)" "λi. iM  ifrFb_body7(B,D,G,r,s,z,i)"])
      from assms aM zM
      have "is_ifrFb_body7(##M, B,D,G, r, s, z, y)  ifrFb_body7(B,D,G, r, s, z, y)" if "yM" for y
        using If_abs apply_0
          separation_closed converse_closed apply_closed range_closed zero_in_M
          transitivity[of _ D] transitivity[of _ G] that sep_dr sep_dr''
        unfolding ifrFb_body7_def is_ifrFb_body7_def
        by auto
      then
      show " y  M  is_ifrFb_body7(##M, B, D, G, r, s, z, y)  y  M  ifrFb_body7(B, D, G, r, s, z, y)" for y
        using conj_cong
        by simp
    qed
    moreover from aM
    have "least(##M, λi. i  M  is_ifrFb_body7(##M, B,D,G, r, s, z, i), a)
       a = (μ i.  i M  is_ifrFb_body7(##M,B,D,G, r, s, z,i))" for z
      using If_abs least_abs'[of "λi. (##M)(i)  is_ifrFb_body7(##M,B,D,G,r,s,z,i)" a]
      by simp
    ultimately
    have "zM  least(##M, λi. i  M  is_ifrFb_body7(##M,B,D,G, r, s, z, i), a)
       a = (μ i. ifrFb_body7(B,D,G, r, s, z,i))" for z
      using Least_cong[OF ifrFb_body7_closed[of B D G r s]] assms
      by simp
  }
  with assms
  show ?thesis
    using  pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
    unfolding ifrangeF_body7_def is_ifrangeF_body7_def
    by (auto dest:transM)
qed

lemma (in M_ZF1_trans) separation_ifrangeF_body7:
  "(##M)(A)  (##M)(B)  (##M)(D)  (##M)(G)  (##M)(b)  (##M)(f) 
    separation(##M,
      λy. xA. y = x, μ i. x  if_range_F_else_F(drSR_Y(B, D, G), b, f, i))"
  using separation_is_ifrangeF_body7 ifrangeF_body7_abs drSR_Y_equality
    separation_cong[where P="is_ifrangeF_body7(##M,A,B,D,G,b,f)" and M="##M",THEN iffD1]
  unfolding ifrangeF_body7_def if_range_F_def if_range_F_else_F_def ifrFb_body7_def
  by simp

definition omfunspace :: "[i,i]  o" where
  "omfunspace(B)  λz. x. nω. zx  x = nB"
relativize functional "omfunspace" "omfunspace_rel"
relationalize "omfunspace_rel" "is_omfunspace"
synthesize "is_omfunspace" from_definition assuming "nonempty"
arity_theorem for "is_omfunspace_fm"

context M_pre_seqspace
begin

is_iff_rel for "omfunspace"
  using is_function_space_iff
  unfolding omfunspace_rel_def is_omfunspace_def
  by (simp add:absolut)

end ― ‹localeM_pre_seqspace

context M_ZF1_trans
begin

lemma separation_omfunspace:
  assumes "(##M)(B)"
  shows "separation(##M, λz. x[##M]. n[##M]. n  ω  z  x  x = n →⇗MB)"
  using assms separation_in_ctm[where env="[B]" and φ="is_omfunspace_fm(1,0)"
      and Q="is_omfunspace(##M,B)"]
    nonempty is_omfunspace_iff[of B, THEN separation_cong, of "##M"]
    arity_is_omfunspace_fm is_omfunspace_fm_type
  unfolding omfunspace_rel_def
  by (auto simp add:ord_simp_union)

end ― ‹localeM_ZF1_trans

sublocale M_ZF1_trans  M_seqspace "##M"
  using separation_omfunspace by unfold_locales

definition cdltgamma :: "[i,i]  o" where
  "cdltgamma(γ)  λZ . |Z| < γ"
relativize functional "cdltgamma" "cdltgamma_rel"
relationalize "cdltgamma_rel" "is_cdltgamma"
synthesize "is_cdltgamma" from_definition assuming "nonempty"
arity_theorem for "is_cdltgamma_fm"

definition cdeqgamma :: "[i]  o" where
  "cdeqgamma  λZ . |fst(Z)| = snd(Z)"
relativize functional "cdeqgamma" "cdeqgamma_rel"
relationalize "cdeqgamma_rel" "is_cdeqgamma"
synthesize "is_cdeqgamma" from_definition assuming "nonempty"
arity_theorem for "is_cdeqgamma_fm"

context M_Perm
begin

is_iff_rel for "cdltgamma"
  using is_cardinal_iff
  unfolding cdltgamma_rel_def is_cdltgamma_def
  by (simp add:absolut)

is_iff_rel for "cdeqgamma"
  using is_cardinal_iff fst_rel_abs snd_rel_abs
  unfolding cdeqgamma_rel_def is_cdeqgamma_def
  by (auto simp add:absolut)

lemma is_cdeqgamma_iff_split: "M(Z)  cdeqgamma_rel(M, Z)  (λx,y. |x|⇗M= y)(Z)"
  using  fst_rel_abs snd_rel_abs
  unfolding cdeqgamma_rel_def split_def
  by simp

end

context M_ZF1_trans
begin

lemma separation_cdltgamma:
  assumes "(##M)(γ)"
  shows "separation(##M, λZ . cardinal_rel(##M,Z) < γ)"
  using assms separation_in_ctm[where env="[γ]" and φ="is_cdltgamma_fm(1,0)"
      and Q="cdltgamma_rel(##M,γ)"]
    nonempty is_cdltgamma_iff[of γ] arity_is_cdltgamma_fm is_cdltgamma_fm_type
  unfolding cdltgamma_rel_def
  by (auto simp add:ord_simp_union)

lemma separation_cdeqgamma:
  shows "separation(##M, λZ. (λx,y . cardinal_rel(##M,x) = y)(Z))"
  using separation_in_ctm[where env="[]" and φ="is_cdeqgamma_fm(0)"
      and Q="cdeqgamma_rel(##M)"] is_cdeqgamma_iff_split
    nonempty is_cdeqgamma_iff arity_is_cdeqgamma_fm is_cdeqgamma_fm_type
    separation_cong[OF is_cdeqgamma_iff_split, of "##M"]
  unfolding cdeqgamma_rel_def
  by (simp add:ord_simp_union)

end ― ‹localeM_ZF1_trans

end