Theory ZF_Miscellanea

sectionVarious results missing from ZF.

theory ZF_Miscellanea
  imports
    ZF
    Nat_Miscellanea
begin

lemma funcI : "f  A  B  a  A  b= f ` a  a, b  f"
  by(simp_all add: apply_Pair)

lemma vimage_fun_sing:
  assumes "fAB" "bB"
  shows "{aA . f`a=b} = f-``{b}"
using assms vimage_singleton_iff function_apply_equality Pi_iff funcI by auto

lemma image_fun_subset: "SAB  CA {S ` x . x C} = S``C"
  using image_function[symmetric,of S C] domain_of_fun Pi_iff by auto

lemma subset_Diff_Un: "X  A  A = (A - X)  X " by auto

lemma Diff_bij:
  assumes "AF. X  A" shows "(λAF. A-X)  bij(F, {A-X. AF})"
  using assms unfolding bij_def inj_def surj_def
  by (auto intro:lam_type, subst subset_Diff_Un[of X]) auto

lemma function_space_nonempty:
  assumes "bB"
  shows "(λxA. b) : A  B"
  using assms lam_type by force

lemma vimage_lam: "(λxA. f(x)) -`` B = { xA . f(x)  B }"
  using lam_funtype[of A f, THEN [2] domain_type]
    lam_funtype[of A f, THEN [2] apply_equality] lamI[of _ A f]
  by auto blast

lemma range_fun_subset_codomain:
  assumes "h:B  C"
  shows "range(h)  C"
  unfolding range_def domain_def converse_def using range_type[OF _ assms]  by auto

lemma Pi_rangeD:
  assumes "fPi(A,B)" "b  range(f)"
  shows "aA. f`a = b"
  using assms apply_equality[OF _ assms(1), of _ b]
    domain_type[OF _ assms(1)] by auto

lemma Pi_range_eq: "f  Pi(A,B)  range(f) = {f ` x . x  A}"
  using Pi_rangeD[of f A B] apply_rangeI[of f A B]
  by blast

lemma Pi_vimage_subset : "f  Pi(A,B)  f-``C  A"
  unfolding Pi_def by auto


definition
  minimum :: "i  i  i" where
  "minimum(r,B)  THE b. first(b,B,r)"

lemma minimum_in: " well_ord(A,r); BA; B0   minimum(r,B)  B"
  using the_first_in unfolding minimum_def by simp

lemma well_ord_surj_imp_inj_inverse:
  assumes "well_ord(A,r)" "h  surj(A,B)"
  shows "(λbB. minimum(r, {aA. h`a=b}))  inj(B,A)"
proof -
  let ?f="λbB. minimum(r, {aA. h`a=b})"
  have "minimum(r, {a  A . h ` a = b})  {aA. h`a=b}" if "bB" for b
  proof -
    from h  surj(A,B) that
    have "{aA. h`a=b}  0"
      unfolding surj_def by blast
    with well_ord(A,r)
    show "minimum(r,{aA. h`a=b})  {aA. h`a=b}"
      using minimum_in by blast
  qed
  moreover from this
  have "?f : B  A"
      using lam_type[of B _ "λ_.A"] by simp
  moreover
  have "?f ` w = ?f ` x  w = x" if "wB" "xB" for w x
  proof -
    from calculation that
    have "w = h ` minimum(r,{aA. h`a=w})"
         "x = h ` minimum(r,{aA. h`a=x})"
      by simp_all
    moreover
    assume "?f ` w = ?f ` x"
    moreover from this and that
    have "minimum(r, {a  A . h ` a = w}) = minimum(r, {a  A . h ` a = x})"
      unfolding minimum_def by simp_all
    moreover from calculation(1,2,4)
    show "w=x" by simp
    qed
  ultimately
  show ?thesis
    unfolding inj_def by blast
qed

lemma well_ord_surj_imp_lepoll:
  assumes "well_ord(A,r)" "h  surj(A,B)"
  shows "BA"
   unfolding lepoll_def using well_ord_surj_imp_inj_inverse[OF assms]
   by blast

― ‹New result
lemma surj_imp_well_ord:
  assumes "well_ord(A,r)" "h  surj(A,B)"
  shows "s. well_ord(B,s)"
  using assms lepoll_well_ord[OF well_ord_surj_imp_lepoll]
  by force

lemma Pow_sing : "Pow({a}) = {0,{a}}"
proof(intro equalityI,simp_all)
  have "z  {0,{a}}" if "z  {a}" for z
    using that by auto
  then
  show " Pow({a})  {0, {a}}" by auto
qed

lemma Pow_cons:
  shows "Pow(cons(a,A)) = Pow(A)  {{a}  X . X: Pow(A)}"
  using Un_Pow_subset Pow_sing
proof(intro equalityI,auto simp add:Un_Pow_subset)
  {
    fix C D
    assume " B . BPow(A)  C  {a}  B" "C  {a}  A" "D  C"
    moreover from this
    have "xC . x=a  xA" by auto
    moreover from calculation
    consider (a) "D=a" | (b) "DA" by auto
    from this
    have "DA"
    proof(cases)
      case a
      with calculation show ?thesis by auto
    next
      case b
      then show ?thesis by simp
    qed
  }
  then show "x xa. (xaPow(A). x  {a}  xa)  x  cons(a, A)  xa  x  xa  A"
    by auto
qed

lemma app_nm :
  assumes "nnat" "mnat" "fnm" "x  nat"
  shows "f`x  nat"
proof(cases "xn")
  case True
  then show ?thesis using assms in_n_in_nat apply_type by simp
next
  case False
  then show ?thesis using assms apply_0 domain_of_fun by simp
qed

lemma Upair_eq_cons: "Upair(a,b) = {a,b}"
  unfolding cons_def by auto

lemma converse_apply_eq : "converse(f) ` x = (f -`` {x})"
  unfolding apply_def vimage_def by simp

lemmas app_fun = apply_iff[THEN iffD1]

lemma Finite_imp_lesspoll_nat:
  assumes "Finite(A)"
  shows "A  nat"
  using assms subset_imp_lepoll[OF naturals_subset_nat] eq_lepoll_trans
    n_lesspoll_nat eq_lesspoll_trans
  unfolding Finite_def lesspoll_def by auto

end