Theory Separation_Instances

theory Separation_Instances
  imports
    Discipline_Function
    Forcing_Data
    FiniteFun_Relative
    Cardinal_Relative
    Replacement_Lepoll
begin

subsection‹More Instances of Separation›
text‹The following instances are mostly the same repetitive task; and we just
copied and pasted, tweaking some lemmas if needed (for example, we might have
needed to use some closedness results).
›

(* FIXME: move these declarations and lemmas where they belong.*)
declare Inl_iff_sats [iff_sats]
declare Inr_iff_sats [iff_sats]
arity_theorem for "Inl_fm"
arity_theorem for "Inr_fm"

arity_theorem for "injection_fm"
arity_theorem for "surjection_fm"
arity_theorem for "bijection_fm"
arity_theorem for "order_isomorphism_fm"
arity_theorem for "pred_set_fm"

(* FIXME: do we need this? does this exists somewhere? *)
lemma iff_sym : "P(x,a) ⟷ a = f(x) ⟹ P(x,a) ⟷ f(x) = a"
  by auto


lemma subset_iff_sats [iff_sats]:
      "[| nth(i,env) = x; nth(k,env) = z;
          i ∈ nat; k ∈ nat; env ∈ list(A)|]
       ==> subset(##A, x, z) ⟷ sats(A, subset_fm(i,k), env)"
  unfolding subset_def subset_fm_def
  by simp


definition radd_body :: "[i,i,i] ⇒ o" where
  "radd_body(R,S) ≡ λz. (∃x y. z = ⟨Inl(x), Inr(y)⟩) ∨
                  (∃x' x. z = ⟨Inl(x'), Inl(x)⟩ ∧ ⟨x', x⟩ ∈ R) ∨
                  (∃y' y. z = ⟨Inr(y'), Inr(y)⟩ ∧ ⟨y', y⟩ ∈ S)"

relativize functional "radd_body" "radd_body_rel"
relationalize "radd_body_rel" "is_radd_body"

synthesize "is_radd_body" from_definition
arity_theorem for "is_radd_body_fm"

lemma (in M_ZF_trans) separation_is_radd_body :
 "(##M)(r) ⟹ (##M)(A) ⟹ separation(##M, is_radd_body(##M,A,r))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,r] ⊨ is_radd_body_fm(1,2,0)",THEN iffD1])
   apply(rule_tac is_radd_body_iff_sats[where env="[_,A,r]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[A,r]",simplified])
    apply(simp_all add:arity_is_radd_body_fm ord_simp_union is_radd_body_fm_type)
  done

lemma (in M_ZF_trans) radd_body_abs :
  assumes "(##M)(R)" "(##M)(S)" "(##M)(x)"
  shows "is_radd_body(##M,R,S,x) ⟷ radd_body(R,S,x)"
  using assms pair_in_M_iff Inl_in_M_iff Inr_in_M_iff
  unfolding radd_body_def is_radd_body_def
  by (auto)

lemma (in M_ZF_trans) separation_radd_body :
 "(##M)(R) ⟹ (##M)(S) ⟹ separation
        (##M, λz. (∃x y. z = ⟨Inl(x), Inr(y)⟩) ∨
                  (∃x' x. z = ⟨Inl(x'), Inl(x)⟩ ∧ ⟨x', x⟩ ∈ R) ∨
                  (∃y' y. z = ⟨Inr(y'), Inr(y)⟩ ∧ ⟨y', y⟩ ∈ S))"
  using separation_is_radd_body radd_body_abs
  unfolding radd_body_def
  by (rule_tac separation_cong[
        where P="is_radd_body(##M,R,S)",THEN iffD1])


definition well_ord_body :: "[i⇒o,i,i,i,i] ⇒ o" where
  "well_ord_body(N,A,f,r,x) ≡ x ∈ A ⟶ (∃y[N]. ∃p[N]. is_apply(N, f, x, y) ∧ pair(N, y, x, p) ∧ p ∈ r)"

synthesize "well_ord_body" from_definition
arity_theorem for "well_ord_body_fm"

lemma (in M_ZF_trans) separation_well_ord_body :
 "(##M)(f) ⟹ (##M)(r) ⟹ (##M)(A) ⟹ separation(##M, well_ord_body(##M,A,f,r))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,f,r] ⊨ well_ord_body_fm(1,2,3,0)",THEN iffD1])
   apply(rule_tac well_ord_body_iff_sats[where env="[_,A,f,r]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[A,f,r]",simplified])
    apply(simp_all add:arity_well_ord_body_fm ord_simp_union well_ord_body_fm_type)
  done

lemma (in M_ZF_trans) separation_well_ord :
 "(##M)(f) ⟹ (##M)(r) ⟹ (##M)(A) ⟹ separation
        (##M, λx. x ∈ A ⟶ (∃y[##M]. ∃p[##M]. is_apply(##M, f, x, y) ∧ pair(##M, y, x, p) ∧ p ∈ r))"
  using separation_well_ord_body well_ord_body_def by simp

definition is_obase_body :: "[i⇒o,i,i,i] ⇒ o" where
  "is_obase_body(N,A,r,x) ≡ x ∈ A ⟶
                  ¬ (∃y[N].
                         ∃g[N].
                            ordinal(N, y) ∧
                            (∃my[N].
                                ∃pxr[N].
                                   membership(N, y, my) ∧
                                   pred_set(N, A, x, r, pxr) ∧
                                   order_isomorphism(N, pxr, r, y, my, g)))"

synthesize "is_obase_body" from_definition
arity_theorem for "is_obase_body_fm"

lemma (in M_ZF_trans) separation_is_obase_body :
 "(##M)(r) ⟹ (##M)(A) ⟹ separation(##M, is_obase_body(##M,A,r))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,r] ⊨ is_obase_body_fm(1,2,0)",THEN iffD1])
   apply(rule_tac is_obase_body_iff_sats[where env="[_,A,r]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[A,r]",simplified])
    apply(simp_all add:arity_is_obase_body_fm ord_simp_union is_obase_body_fm_type)
  done

lemma (in M_ZF_trans) separation_is_obase :
 "(##M)(f) ⟹ (##M)(r) ⟹ (##M)(A) ⟹ separation
        (##M, λx. x ∈ A ⟶
                  ¬ (∃y[##M].
                         ∃g[##M].
                            ordinal(##M, y) ∧
                            (∃my[##M].
                                ∃pxr[##M].
                                   membership(##M, y, my) ∧
                                   pred_set(##M, A, x, r, pxr) ∧
                                   order_isomorphism(##M, pxr, r, y, my, g))))"
  using separation_is_obase_body is_obase_body_def by simp

definition is_obase_equals :: "[i⇒o,i,i,i] ⇒ o" where
  "is_obase_equals(N,A,r,a) ≡ ∃x[N].
                     ∃g[N].
                        ∃mx[N].
                           ∃par[N].
                              ordinal(N, x) ∧
                              membership(N, x, mx) ∧
                              pred_set(N, A, a, r, par) ∧ order_isomorphism(N, par, r, x, mx, g)"

synthesize "is_obase_equals" from_definition
arity_theorem for "is_obase_equals_fm"

lemma (in M_ZF_trans) separation_obase_equals_aux :
 "(##M)(r) ⟹ (##M)(A) ⟹ separation(##M, is_obase_equals(##M,A,r))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,r] ⊨ is_obase_equals_fm(1,2,0)",THEN iffD1])
   apply(rule_tac is_obase_equals_iff_sats[where env="[_,A,r]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[A,r]",simplified])
    apply(simp_all add:arity_is_obase_equals_fm ord_simp_union is_obase_equals_fm_type)
  done

lemma (in M_ZF_trans) separation_obase_equals :
 "(##M)(f) ⟹ (##M)(r) ⟹ (##M)(A) ⟹ separation
        (##M, λa. ∃x[##M].
                     ∃g[##M].
                        ∃mx[##M].
                           ∃par[##M].
                              ordinal(##M, x) ∧
                              membership(##M, x, mx) ∧
                              pred_set(##M, A, a, r, par) ∧ order_isomorphism(##M, par, r, x, mx, g))"
  using separation_obase_equals_aux is_obase_equals_def by (simp)


definition id_body :: "[i,i] ⇒ o" where
  "id_body(A) ≡ λz. ∃x∈A. z = ⟨x, x⟩"
relativize "id_body" "is_id_body"
synthesize "is_id_body" from_definition assuming "nonempty"
arity_theorem for "is_id_body_fm"

lemma (in M_ZF_trans) separation_is_id_body :
 "(##M)(A) ⟹ separation(##M, is_id_body(##M,A))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A] ⊨ is_id_body_fm(1,0)",THEN iffD1])
   apply(rule_tac is_id_body_iff_sats[where env="[_,A]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A]",simplified])
    apply(simp_all add:arity_is_id_body_fm ord_simp_union is_id_body_fm_type)
  done

lemma (in M_ZF_trans) id_body_abs :
  assumes "(##M)(A)" "(##M)(x)"
  shows "is_id_body(##M,A,x) ⟷ id_body(A,x)"
  using assms zero_in_M pair_in_M_iff unfolding id_body_def is_id_body_def
  by auto

lemma (in M_ZF_trans) separation_id_body :
 "(##M)(A) ⟹ separation
        (##M, λz. ∃x∈A. z = ⟨x, x⟩)"
  using id_body_abs separation_is_id_body
  unfolding id_body_def
  by (rule_tac separation_cong[where P="is_id_body(##M,A)",THEN iffD1])

definition rvimage_body :: "[i,i,i] ⇒ o" where
  "rvimage_body(f,r) ≡ λz. ∃x y. z = ⟨x, y⟩ ∧ ⟨f ` x, f ` y⟩ ∈ r"

relativize functional "rvimage_body" "rvimage_body_rel"
relationalize "rvimage_body_rel" "is_rvimage_body"

synthesize "is_rvimage_body" from_definition
arity_theorem for "is_rvimage_body_fm"

lemma (in M_ZF_trans) separation_is_rvimage_body :
 "(##M)(f) ⟹ (##M)(r) ⟹ separation(##M, is_rvimage_body(##M,f,r))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,f,r] ⊨ is_rvimage_body_fm(1,2,0)",THEN iffD1])
   apply(rule_tac is_rvimage_body_iff_sats[where env="[_,f,r]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[f,r]",simplified])
    apply(simp_all add:arity_is_rvimage_body_fm ord_simp_union is_rvimage_body_fm_type)
  done

lemma (in M_ZF_trans) rvimage_body_abs :
  assumes "(##M)(R)" "(##M)(S)" "(##M)(x)"
  shows "is_rvimage_body(##M,R,S,x) ⟷ rvimage_body(R,S,x)"
  using assms pair_in_M_iff apply_closed
  unfolding rvimage_body_def is_rvimage_body_def
  by (auto)

lemma (in M_ZF_trans) separation_rvimage_body :
 "(##M)(f) ⟹ (##M)(r) ⟹ separation
        (##M, λz. ∃x y. z = ⟨x, y⟩ ∧ ⟨f ` x, f ` y⟩ ∈ r)"
  using separation_is_rvimage_body rvimage_body_abs
  unfolding rvimage_body_def
  by (rule_tac separation_cong[
        where P="is_rvimage_body(##M,f,r)",THEN iffD1])

(* rmult_separation *)

definition rmult_body :: "[i,i,i] ⇒ o" where
  "rmult_body(b,d) ≡ λz. ∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ b ∨ x' = x ∧ ⟨y', y⟩ ∈ d)"

relativize functional "rmult_body" "rmult_body_rel"
relationalize "rmult_body_rel" "is_rmult_body"

synthesize "is_rmult_body" from_definition
arity_theorem for "is_rmult_body_fm"

lemma (in M_ZF_trans) separation_is_rmult_body :
 "(##M)(b) ⟹ (##M)(d) ⟹ separation(##M, is_rmult_body(##M,b,d))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,b,d] ⊨ is_rmult_body_fm(1,2,0)",THEN iffD1])
   apply(rule_tac is_rmult_body_iff_sats[where env="[_,b,d]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[b,d]",simplified])
    apply(simp_all add:arity_is_rmult_body_fm ord_simp_union is_rmult_body_fm_type)
  done

lemma (in M_ZF_trans) rmult_body_abs :
  assumes "(##M)(b)" "(##M)(d)" "(##M)(x)"
  shows "is_rmult_body(##M,b,d,x) ⟷ rmult_body(b,d,x)"
  using assms pair_in_M_iff apply_closed
  unfolding rmult_body_def is_rmult_body_def
  by (auto)

lemma (in M_ZF_trans) separation_rmult_body :
 "(##M)(b) ⟹ (##M)(d) ⟹ separation
        (##M, λz. ∃x' y' x y. z = ⟨⟨x', y'⟩, x, y⟩ ∧ (⟨x', x⟩ ∈ b ∨ x' = x ∧ ⟨y', y⟩ ∈ d))"
  using separation_is_rmult_body rmult_body_abs
    separation_cong[where P="is_rmult_body(##M,b,d)" and M="##M",THEN iffD1]
  unfolding rmult_body_def
  by simp

definition ord_iso_body :: "[i,i,i,i] ⇒ o" where
  "ord_iso_body(A,r,s) ≡ λf. ∀x∈A. ∀y∈A. ⟨x, y⟩ ∈ r ⟷ ⟨f ` x, f ` y⟩ ∈ s"

relativize functional "ord_iso_body" "ord_iso_body_rel"
relationalize "ord_iso_body_rel" "is_ord_iso_body"

synthesize "is_ord_iso_body" from_definition assuming "nonempty"
arity_theorem for "is_ord_iso_body_fm"

lemma (in M_ZF_trans) separation_is_ord_iso_body :
 "(##M)(A) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ord_iso_body(##M,A,r,s))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,r,s] ⊨ is_ord_iso_body_fm(1,2,3,0)",THEN iffD1])
   apply(rule_tac is_ord_iso_body_iff_sats[where env="[_,A,r,s]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,r,s]",simplified])
    apply(simp_all add:arity_is_ord_iso_body_fm ord_simp_union is_ord_iso_body_fm_type)
  done

lemma (in M_ZF_trans) ord_iso_body_abs :
  assumes "(##M)(A)" "(##M)(r)" "(##M)(s)" "(##M)(x)"
  shows "is_ord_iso_body(##M,A,r,s,x) ⟷ ord_iso_body(A,r,s,x)"
  using assms pair_in_M_iff apply_closed zero_in_M transitivity[of _ A]
  unfolding ord_iso_body_def is_ord_iso_body_def
  by auto

lemma (in M_ZF_trans) separation_ord_iso_body :
 "(##M)(A) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation
        (##M, λf. ∀x∈A. ∀y∈A. ⟨x, y⟩ ∈ r ⟷ ⟨f ` x, f ` y⟩ ∈ s)"
  using separation_is_ord_iso_body ord_iso_body_abs
    separation_cong[where P="is_ord_iso_body(##M,A,r,s)" and M="##M",THEN iffD1]
  unfolding ord_iso_body_def
  by simp


synthesize "PiP_rel" from_definition assuming "nonempty"
arity_theorem for "PiP_rel_fm"

lemma (in M_ZF_trans) separation_PiP_rel :
 "(##M)(A) ⟹ separation(##M, PiP_rel(##M,A))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A] ⊨ PiP_rel_fm(1,0)",THEN iffD1])
   apply(rule_tac PiP_rel_iff_sats[where env="[_,A]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A]",simplified])
    apply(simp_all add:arity_PiP_rel_fm ord_simp_union PiP_rel_fm_type)
  done

synthesize "injP_rel" from_definition assuming "nonempty"
arity_theorem for "injP_rel_fm"

lemma (in M_ZF_trans) separation_injP_rel :
 "(##M)(A) ⟹ separation(##M, injP_rel(##M,A))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A] ⊨ injP_rel_fm(1,0)",THEN iffD1])
   apply(rule_tac injP_rel_iff_sats[where env="[_,A]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A]",simplified])
    apply(simp_all add:arity_injP_rel_fm ord_simp_union injP_rel_fm_type)
  done

synthesize "surjP_rel" from_definition assuming "nonempty"
arity_theorem for "surjP_rel_fm"

lemma (in M_ZF_trans) separation_surjP_rel :
 "(##M)(A) ⟹ (##M)(B) ⟹ separation(##M, surjP_rel(##M,A,B))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,B] ⊨ surjP_rel_fm(1,2,0)",THEN iffD1])
   apply(rule_tac surjP_rel_iff_sats[where env="[_,A,B]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,B]",simplified])
    apply(simp_all add:arity_surjP_rel_fm ord_simp_union surjP_rel_fm_type)
  done

synthesize "cons_like_rel" from_definition assuming "nonempty"
arity_theorem for "cons_like_rel_fm"

lemma (in M_ZF_trans) separation_cons_like_rel :
 "separation(##M, cons_like_rel(##M))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x] ⊨ cons_like_rel_fm(0)",THEN iffD1])
   apply(rule_tac cons_like_rel_iff_sats[where env="[_]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[]",simplified])
    apply(simp_all add:arity_cons_like_rel_fm ord_simp_union cons_like_rel_fm_type)
  done

definition supset_body :: "[i] ⇒ o" where
  "supset_body ≡ λ x. ∃a. ∃b. x = ⟨a,b⟩ ∧ b ⊆ a"

relativize functional "supset_body" "supset_body_rel"
relationalize "supset_body_rel" "is_supset_body"

synthesize "is_supset_body" from_definition
arity_theorem for "is_supset_body_fm"

lemma (in M_ZF_trans) separation_is_supset_body :
 "separation(##M, is_supset_body(##M))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x] ⊨ is_supset_body_fm(0)",THEN iffD1])
   apply(rule_tac is_supset_body_iff_sats[where env="[_]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[]",simplified])
    apply(simp_all add:arity_is_supset_body_fm ord_simp_union is_supset_body_fm_type)
  done

lemma (in M_ZF_trans) supset_body_abs :
  assumes "(##M)(x)"
  shows "is_supset_body(##M,x) ⟷ supset_body(x)"
  using assms pair_in_M_iff apply_closed
  unfolding supset_body_def is_supset_body_def
  by (auto)

lemma (in M_ZF_trans) separation_supset_body :
 "separation(##M, λ x. ∃a. ∃b. x = ⟨a,b⟩ ∧ b ⊆ a)"
  using separation_is_supset_body supset_body_abs
    separation_cong[where P="is_supset_body(##M)" and M="##M",THEN iffD1]
  unfolding supset_body_def
  by simp

lemma (in M_ZF_trans) separation_is_fst :
 "(##M)(a) ⟹ separation(##M, λx . is_fst(##M,x,a))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,a] ⊨ fst_fm(0,1)",THEN iffD1])
   apply(rule_tac fst_iff_sats[where env="[_,a]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[a]",simplified])
    apply(simp_all add:arity_fst_fm ord_simp_union fst_fm_type)
  done

lemma (in M_ZF_trans) separation_fst_equal :
 "(##M)(a) ⟹ separation(##M, λx. fst(x) = a)"
  using separation_cong[THEN iffD1,OF _ separation_is_fst[of a]]
     iff_sym[of "is_fst(##M)" _ a "fst", OF fst_abs]
  by auto

lemma (in M_ZF_trans) separation_is_apply :
 "(##M)(f) ⟹ (##M)(a) ⟹ separation(##M, λx . is_apply(##M,f,x,a))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,f,a] ⊨ fun_apply_fm(1,0,2)",THEN iffD1])
   apply(rule_tac fun_apply_iff_sats[where env="[_,f,a]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[f,a]",simplified])
    apply(simp_all add:arity_fun_apply_fm ord_simp_union)
  done

lemma (in M_ZF_trans) separation_equal_apply :
 "(##M)(f) ⟹ (##M)(a) ⟹ separation(##M, λx. f`x = a)"
  using separation_cong[THEN iffD1,OF _ separation_is_apply[of f a]] apply_abs
  by force
(* *)
definition id_rel :: "[i⇒o,i] ⇒ o" where
  "id_rel(A) ≡ λz. ∃x[A]. z = ⟨x, x⟩"
relativize "id_rel" "is_id_rel"
synthesize "is_id_rel" from_definition assuming "nonempty"
arity_theorem for "is_id_rel_fm"

lemma (in M_ZF_trans) separation_is_id_rel :
 "separation(##M, is_id_rel(##M))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x] ⊨ is_id_rel_fm(0)",THEN iffD1])
   apply(rule_tac is_id_rel_iff_sats[where env="[_]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[]",simplified])
    apply(simp_all add:arity_is_id_rel_fm ord_simp_union is_id_rel_fm_type)
  done

lemma (in M_ZF_trans) id_rel_abs :
  assumes "(##M)(x)"
  shows "is_id_rel(##M,x) ⟷ id_rel(##M,x)"
  using assms zero_in_M pair_in_M_iff unfolding id_rel_def is_id_rel_def
  by auto

lemma (in M_ZF_trans) separation_id_rel :
 "separation(##M, λz. ∃x[##M]. z = ⟨x, x⟩)"
  using id_rel_abs separation_is_id_rel
  unfolding id_rel_def
  by (rule_tac separation_cong[where P="is_id_rel(##M)",THEN iffD1])


 (* 2. separation(##M, λx. snd(fst(x)) = fst(snd(x))) *)
definition sndfst_eq_fstsnd :: "[i] ⇒ o" where
  "sndfst_eq_fstsnd ≡ λx. snd(fst(x)) = fst(snd(x))"
relativize "sndfst_eq_fstsnd" "is_sndfst_eq_fstsnd"
synthesize "is_sndfst_eq_fstsnd" from_definition assuming "nonempty"
arity_theorem for "is_sndfst_eq_fstsnd_fm"

lemma (in M_ZF_trans) separation_is_sndfst_eq_fstsnd :
 "separation(##M, is_sndfst_eq_fstsnd(##M))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x] ⊨ is_sndfst_eq_fstsnd_fm(0)",THEN iffD1])
   apply(rule_tac is_sndfst_eq_fstsnd_iff_sats[where env="[_]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[]",simplified])
    apply(simp_all add:arity_is_sndfst_eq_fstsnd_fm ord_simp_union is_sndfst_eq_fstsnd_fm_type)
  done

lemma (in M_ZF_trans) sndfst_eq_fstsnd_abs :
  assumes "(##M)(x)"
  shows "is_sndfst_eq_fstsnd(##M,x) ⟷ sndfst_eq_fstsnd(x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
  unfolding sndfst_eq_fstsnd_def is_sndfst_eq_fstsnd_def
  by auto

lemma (in M_ZF_trans) separation_sndfst_eq_fstsnd :
 "separation(##M, λx. snd(fst(x)) = fst(snd(x)))"
  using sndfst_eq_fstsnd_abs separation_is_sndfst_eq_fstsnd
  unfolding sndfst_eq_fstsnd_def
  by (rule_tac separation_cong[where P="is_sndfst_eq_fstsnd(##M)",THEN iffD1])



 (* 3. separation(##M, λx. fst(fst(x)) = fst(snd(x))) *)
definition fstfst_eq_fstsnd :: "[i] ⇒ o" where
  "fstfst_eq_fstsnd ≡ λx. fst(fst(x)) = fst(snd(x))"
relativize "fstfst_eq_fstsnd" "is_fstfst_eq_fstsnd"
synthesize "is_fstfst_eq_fstsnd" from_definition assuming "nonempty"
arity_theorem for "is_fstfst_eq_fstsnd_fm"

lemma (in M_ZF_trans) separation_is_fstfst_eq_fstsnd :
 "separation(##M, is_fstfst_eq_fstsnd(##M))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x] ⊨ is_fstfst_eq_fstsnd_fm(0)",THEN iffD1])
   apply(rule_tac is_fstfst_eq_fstsnd_iff_sats[where env="[_]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[]",simplified])
    apply(simp_all add:arity_is_fstfst_eq_fstsnd_fm ord_simp_union is_fstfst_eq_fstsnd_fm_type)
  done

lemma (in M_ZF_trans) fstfst_eq_fstsnd_abs :
  assumes "(##M)(x)"
  shows "is_fstfst_eq_fstsnd(##M,x) ⟷ fstfst_eq_fstsnd(x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
  unfolding fstfst_eq_fstsnd_def is_fstfst_eq_fstsnd_def
  by auto

lemma (in M_ZF_trans) separation_fstfst_eq_fstsnd :
 "separation(##M, λx. fst(fst(x)) = fst(snd(x)))"
  using fstfst_eq_fstsnd_abs separation_is_fstfst_eq_fstsnd
  unfolding fstfst_eq_fstsnd_def
  by (rule_tac separation_cong[where P="is_fstfst_eq_fstsnd(##M)",THEN iffD1])


 (* 5. ⋀a. (##M)(a) ⟹ separation(##M, λx. fst(fst(x)) = a) *)
definition fstfst_eq :: "[i,i] ⇒ o" where
  "fstfst_eq(a) ≡ λx. fst(fst(x)) = a"

relativize "fstfst_eq" "is_fstfst_eq"
synthesize "is_fstfst_eq" from_definition assuming "nonempty"
arity_theorem for "is_fstfst_eq_fm"

lemma (in M_ZF_trans) separation_is_fstfst_eq :
 "(##M)(a) ⟹ separation(##M, is_fstfst_eq(##M,a))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,a] ⊨ is_fstfst_eq_fm(1,0)",THEN iffD1])
   apply(rule_tac is_fstfst_eq_iff_sats[where env="[_,a]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[a]",simplified])
    apply(simp_all add:arity_is_fstfst_eq_fm ord_simp_union is_fstfst_eq_fm_type)
  done

lemma (in M_ZF_trans) fstfst_eq_abs :
  assumes "(##M)(a)" "(##M)(x)"
  shows "is_fstfst_eq(##M,a,x) ⟷ fstfst_eq(a,x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
  unfolding fstfst_eq_def is_fstfst_eq_def
  by auto

lemma (in M_ZF_trans) separation_fstfst_eq :
 "(##M)(a) ⟹ separation(##M, λx. fst(fst(x)) = a)"
  using fstfst_eq_abs separation_is_fstfst_eq
  unfolding fstfst_eq_def
  by (rule_tac separation_cong[where P="is_fstfst_eq(##M,a)",THEN iffD1])


(*⋀B. (##M)(B) ⟹ ∀A∈M. separation(##M, λy. ∃x∈A. y = ⟨x, restrict(x, B)⟩)*)
definition restrict_elem :: "[i,i,i] ⇒ o" where
  "restrict_elem(B,A) ≡ λy. ∃x∈A. y = ⟨x, restrict(x, B)⟩"

relativize "restrict_elem" "is_restrict_elem"
synthesize "is_restrict_elem" from_definition assuming "nonempty"
arity_theorem for "is_restrict_elem_fm"

lemma (in M_ZF_trans) separation_is_restrict_elem :
 "(##M)(B) ⟹ (##M)(A) ⟹ separation(##M, is_restrict_elem(##M,B,A))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,B] ⊨ is_restrict_elem_fm(2,1,0)",THEN iffD1])
   apply(rule_tac is_restrict_elem_iff_sats[where env="[_,A,B]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,B]",simplified])
    apply(simp_all add:arity_is_restrict_elem_fm ord_simp_union is_restrict_elem_fm_type)
  done

lemma (in M_ZF_trans) restrict_elem_abs :
  assumes "(##M)(B)" "(##M)(A)" "(##M)(x)"
  shows "is_restrict_elem(##M,B,A,x) ⟷ restrict_elem(B,A,x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
  unfolding restrict_elem_def is_restrict_elem_def
  by auto

lemma (in M_ZF_trans) separation_restrict_elem_aux :
 "(##M)(B) ⟹ (##M)(A) ⟹ separation(##M, λy. ∃x∈A. y = ⟨x, restrict(x, B)⟩)"
  using restrict_elem_abs separation_is_restrict_elem
  unfolding restrict_elem_def
  by (rule_tac separation_cong[where P="is_restrict_elem(##M,B,_)",THEN iffD1])

lemma (in M_ZF_trans) separation_restrict_elem :
 "(##M)(B) ⟹ ∀A[##M]. separation(##M, λy. ∃x∈A. y = ⟨x, restrict(x, B)⟩)"
  using separation_restrict_elem_aux by simp

lemma (in M_ZF_trans) separation_ordinal :
 "separation(##M, ordinal(##M))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x] ⊨ ordinal_fm(0)",THEN iffD1])
   apply(rule_tac ordinal_iff_sats[where env="[_]",symmetric])
  apply(simp_all)
  apply(rule_tac separation_ax[where env="[]",simplified])
    apply(simp_all add:ord_simp_union )
  done

lemma (in M_ZF_trans) separation_Ord :
 "separation(##M, Ord)"
  using separation_ordinal ordinal_abs
    separation_cong[where P="ordinal(##M)" and M="##M",THEN iffD1]
  unfolding Ord_def
  by simp

(*  "M(G) ⟹ M(Q) ⟹ separation(M, λp. ∀x∈G. x ∈ snd(p) ⟷ (∀s∈fst(p). ⟨s, x⟩ ∈ Q))" *)
definition insnd_ballPair :: "[i,i,i] ⇒ o" where
  "insnd_ballPair(B,A) ≡ λp. ∀x∈B. x ∈ snd(p) ⟷ (∀s∈fst(p). ⟨s, x⟩ ∈ A)"

relativize "insnd_ballPair" "is_insnd_ballPair"
synthesize "is_insnd_ballPair" from_definition assuming "nonempty"
arity_theorem for "is_insnd_ballPair_fm"

lemma (in M_ZF_trans) separation_is_insnd_ballPair :
 "(##M)(B) ⟹ (##M)(A) ⟹ separation(##M, is_insnd_ballPair(##M,B,A))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,B] ⊨ is_insnd_ballPair_fm(2,1,0)",THEN iffD1])
   apply(rule_tac is_insnd_ballPair_iff_sats[where env="[_,A,B]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,B]",simplified])
    apply(simp_all add:arity_is_insnd_ballPair_fm ord_simp_union is_insnd_ballPair_fm_type)
  done

lemma (in M_ZF_trans) insnd_ballPair_abs :
  assumes "(##M)(B)" "(##M)(A)" "(##M)(x)"
  shows "is_insnd_ballPair(##M,B,A,x) ⟷ insnd_ballPair(B,A,x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed
    transM[of _ B] transM[of _ "snd(x)"] transM[of _ "fst(x)"]
  unfolding insnd_ballPair_def is_insnd_ballPair_def
  by (auto)

lemma (in M_ZF_trans) separation_insnd_ballPair_aux :
 "(##M)(B) ⟹ (##M)(A) ⟹ separation(##M, λp. ∀x∈B. x ∈ snd(p) ⟷ (∀s∈fst(p). ⟨s, x⟩ ∈ A))"
  using insnd_ballPair_abs separation_is_insnd_ballPair
  unfolding insnd_ballPair_def
  by (rule_tac separation_cong[where P="is_insnd_ballPair(##M,B,_)",THEN iffD1])

lemma (in M_ZF_trans) separation_insnd_ballPair :
 "(##M)(B) ⟹ ∀A[##M]. separation(##M, λp. ∀x∈B. x ∈ snd(p) ⟷ (∀s∈fst(p). ⟨s, x⟩ ∈ A))"
  using separation_insnd_ballPair_aux by simp

(* *)
definition bex_restrict_eq_dom :: "[i,i,i,i] ⇒ o" where
  "bex_restrict_eq_dom(B,A,x) ≡ λdr. ∃r∈A . restrict(r,B) = x ∧ dr=domain(r)"

relativize "bex_restrict_eq_dom" "is_bex_restrict_eq_dom"
synthesize "is_bex_restrict_eq_dom" from_definition assuming "nonempty"
arity_theorem for "is_bex_restrict_eq_dom_fm"

lemma (in M_ZF_trans) separation_is_bex_restrict_eq_dom :
 "(##M)(B) ⟹ (##M)(A) ⟹ (##M)(x) ⟹ separation(##M, is_bex_restrict_eq_dom(##M,B,A,x))"
  apply(rule_tac separation_cong[
        where P="λ dr . M,[dr,x,A,B] ⊨ is_bex_restrict_eq_dom_fm(3,2,1,0)",THEN iffD1])
   apply(rule_tac is_bex_restrict_eq_dom_iff_sats[where env="[_,x,A,B]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[x,A,B]",simplified])
    apply(simp_all add:arity_is_bex_restrict_eq_dom_fm ord_simp_union is_bex_restrict_eq_dom_fm_type)
  done
lemma (in M_ZF_trans) bex_restrict_eq_dom_abs :
  assumes "(##M)(B)" "(##M)(A)" "(##M)(x)" "(##M)(dr)"
  shows "is_bex_restrict_eq_dom(##M,B,A,x,dr) ⟷ bex_restrict_eq_dom(B,A,x,dr)"
  using assms transM[of _ B] transM[of _ A]
  unfolding bex_restrict_eq_dom_def is_bex_restrict_eq_dom_def 
  by (auto)

lemma (in M_ZF_trans) separation_restrict_eq_dom_eq_aux : 
    "(##M)(A) ⟹ (##M)(B) ⟹ (##M)(x) ⟹ separation(##M, λdr. ∃r∈A . restrict(r,B) = x ∧ dr=domain(r))" 
  using bex_restrict_eq_dom_abs separation_is_bex_restrict_eq_dom
  unfolding bex_restrict_eq_dom_def
  by (rule_tac separation_cong[where P="is_bex_restrict_eq_dom(##M,B,A,x)",THEN iffD1])

lemma (in M_ZF_trans) separation_restrict_eq_dom_eq : 
    "(##M)(A) ⟹ (##M)(B) ⟹ ∀x[##M]. separation(##M, λdr. ∃r∈A . restrict(r,B) = x ∧ dr=domain(r))" 
  using separation_restrict_eq_dom_eq_aux by simp

definition insnd_restrict_eq_dom :: "[i,i,i,i] ⇒ o" where
  "insnd_restrict_eq_dom(B,A,D) ≡ λp. ∀x∈D. x ∈ snd(p) ⟷ (∃r∈A. restrict(r, B) = fst(p) ∧ x = domain(r))"

definition is_insnd_restrict_eq_dom :: "[i⇒o,i,i,i,i] ⇒ o" where
  "is_insnd_restrict_eq_dom(N,B,A,D,p) ≡
       ∃c[N].
          ∃a[N].
             (∀x[N]. x ∈ D ⟶ x ∈ a ⟷ (∃r[N]. ∃b[N]. (r ∈ A ∧restriction(N, r, B, b)) ∧ b=c ∧ is_domain(N, r, x))) ∧
             is_snd(N, p, a) ∧ is_fst(N, p, c)"

synthesize "is_insnd_restrict_eq_dom" from_definition assuming "nonempty"
arity_theorem for "is_insnd_restrict_eq_dom_fm"

lemma (in M_ZF_trans) separation_is_insnd_restrict_eq_dom :
 "(##M)(B) ⟹ (##M)(A) ⟹ (##M)(D) ⟹ separation(##M, is_insnd_restrict_eq_dom(##M,B,A,D))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,D,A,B] ⊨ is_insnd_restrict_eq_dom_fm(3,2,1,0)",THEN iffD1])
   apply(rule_tac is_insnd_restrict_eq_dom_iff_sats[where env="[_,D,A,B]",symmetric])
  apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[D,A,B]",simplified])
    apply(simp_all add:arity_is_insnd_restrict_eq_dom_fm ord_simp_union is_insnd_restrict_eq_dom_fm_type)
  done

lemma (in M_basic) insnd_restrict_eq_dom_abs :
  assumes "(M)(B)" "(M)(A)" "(M)(D)" "(M)(x)"
  shows "is_insnd_restrict_eq_dom(M,B,A,D,x) ⟷ insnd_restrict_eq_dom(B,A,D,x)"
  using assms pair_in_M_iff fst_abs snd_abs fst_snd_closed domain_closed
    transM[of _ B] transM[of _ D] transM[of _ A]  transM[of _ "snd(x)"] transM[of _ "fst(x)"]
  unfolding insnd_restrict_eq_dom_def is_insnd_restrict_eq_dom_def
  by simp

lemma (in M_ZF_trans) separation_restrict_eq_dom_eq_pair_aux :
    "(##M)(A) ⟹ (##M)(B) ⟹ (##M)(D) ⟹
      separation(##M, λp. ∀x∈D. x ∈ snd(p) ⟷ (∃r∈A. restrict(r, B) = fst(p) ∧ x = domain(r)))"
  using separation_is_insnd_restrict_eq_dom insnd_restrict_eq_dom_abs
  unfolding insnd_restrict_eq_dom_def
  by (rule_tac separation_cong[where P="is_insnd_restrict_eq_dom(##M,B,A,D)",THEN iffD1])

lemma (in M_ZF_trans) separation_restrict_eq_dom_eq_pair :
    "(##M)(A) ⟹ (##M)(B) ⟹ 
  ∀D[##M]. separation(##M, λp. ∀x∈D. x ∈ snd(p) ⟷ (∃r∈A. restrict(r, B) = fst(p) ∧ x = domain(r)))" 
  using separation_restrict_eq_dom_eq_pair_aux by simp

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

(* MOVE THIS to an appropriate place *)
synthesize "is_converse" from_definition assuming "nonempty"
arity_theorem for "is_converse_fm"

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 :: "[i⇒o,i,i,i,i] ⇒ o" where
  "ifrangeF_body(M,A,b,f) ≡ λy. ∃x∈A. 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_ZF_trans) separation_is_ifrangeF_body :
  "(##M)(A) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body(##M,A,r,s))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,r,s] ⊨ is_ifrangeF_body_fm(1,2,3,0)",THEN iffD1])
   apply(rule_tac is_ifrangeF_body_iff_sats[where env="[_,A,r,s]",symmetric])
            apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,r,s]",simplified])
    apply(simp_all add:arity_is_ifrangeF_body_fm ord_simp_union is_ifrangeF_body_fm_type)
  done

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 "i∈range(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF_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 "a∈M"
    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. i∈M ∧ 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 ‹a∈M›
      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 "y∈M"; cases "y∈range(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 ‹a∈M›
    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_ZF_trans) separation_ifrangeF_body :
  "(##M)(A) ⟹ (##M)(b) ⟹ (##M)(f) ⟹ separation
        (##M, λy.  ∃x∈A. 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 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "ifrangeF_body2(M,A,G,b,f) ≡ λy. ∃x∈A. 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_ZF_trans) separation_is_ifrangeF_body2 :
  "(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body2(##M,A,G,r,s))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,G,r,s] ⊨ is_ifrangeF_body2_fm(1,2,3,4,0)",THEN iffD1])
   apply(rule_tac is_ifrangeF_body2_iff_sats[where env="[_,A,G,r,s]",symmetric])
              apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,G,r,s]",simplified])
    apply(simp_all add:arity_is_ifrangeF_body2_fm ord_simp_union is_ifrangeF_body2_fm_type)
  done

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 "i∈range(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF_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 "a∈M"
    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. i∈M ∧ 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 ‹a∈M›
      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 "y∈M"; cases "y∈range(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 ‹a∈M›
    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_ZF_trans) separation_ifrangeF_body2 :
  "(##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)⟩)"
  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 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "ifrangeF_body3(M,A,G,b,f) ≡ λy. ∃x∈A. 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_ZF_trans) separation_is_ifrangeF_body3 :
  "(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body3(##M,A,G,r,s))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,G,r,s] ⊨ is_ifrangeF_body3_fm(1,2,3,4,0)",THEN iffD1])
   apply(rule_tac is_ifrangeF_body3_iff_sats[where env="[_,A,G,r,s]",symmetric])
              apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,G,r,s]",simplified])
    apply(simp_all add:arity_is_ifrangeF_body3_fm ord_simp_union is_ifrangeF_body3_fm_type)
  done

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 "i∈range(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF_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 "a∈M"
    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. i∈M ∧ 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 ‹a∈M›
      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 "y∈M"; cases "y∈range(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 ‹a∈M›
    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_ZF_trans) separation_ifrangeF_body3 :
  "(##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)⟩)"
  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 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "ifrangeF_body4(M,A,G,b,f) ≡ λy. ∃x∈A. 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_ZF_trans) separation_is_ifrangeF_body4 :
  "(##M)(A) ⟹ (##M)(G) ⟹ (##M)(r) ⟹ (##M)(s) ⟹ separation(##M, is_ifrangeF_body4(##M,A,G,r,s))"
  apply(rule_tac separation_cong[
        where P="λ x . M,[x,A,G,r,s] ⊨ is_ifrangeF_body4_fm(1,2,3,4,0)",THEN iffD1])
   apply(rule_tac is_ifrangeF_body4_iff_sats[where env="[_,A,G,r,s]",symmetric])
              apply(simp_all add:zero_in_M)
  apply(rule_tac separation_ax[where env="[A,G,r,s]",simplified])
    apply(simp_all add:arity_is_ifrangeF_body4_fm ord_simp_union is_ifrangeF_body4_fm_type)
  done

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 "i∈range(s)"; cases "r=0"; auto dest:transM)

lemma (in M_ZF_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 "a∈M"
    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. i∈M ∧ 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 "z∈M" 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 ‹a∈M› ‹z∈M›
      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 "y∈M"; cases "y∈range(s)"; cases "r=0"; cases "y∈domain(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 ‹a∈M›
    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 "z∈M ⟹ 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_ZF_trans) separation_ifrangeF_body4 :
  "(##M)(A) ⟹ (##M)(G) ⟹ (##M)(b) ⟹ (##M)(f) ⟹
       separation(##M, λy. ∃x∈A. 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 :: "[i⇒o,i,i,i,i,i] ⇒ o" where
  "ifrangeF_body5(M,A,G,b,f) ≡ λy. ∃x∈A. y = ⟨x,μ i. ifrFb_body5(G,b,f,x,i