# Theory equalities

Up to index of Isabelle/ZF

theory equalities
imports pair
begin

    (*  Title:      ZF/equalities
        ID:         $Id: equalities.thy,v 1.27 2005/06/17 14:15:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1992  University of Cambridge

    *)

    header{*Basic Equalities and Inclusions*}

    theory equalities imports pair begin

    text{*These cover union, intersection, converse, domain, range, etc.  Philippe
    de Groote proved many of the inclusions.*}

    lemma in_mono: "A⊆B ==> x∈A --> x∈B"
    by blast

    lemma the_eq_0 [simp]: "(THE x. False) = 0"
    by (blast intro: the_0)

    subsection{*Bounded Quantifiers*}
    text {* \medskip

      The following are not added to the default simpset because
      (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}

    lemma ball_Un: "(∀x ∈ A∪B. P(x)) <-> (∀x ∈ A. P(x)) & (∀x ∈ B. P(x))";
      by blast

    lemma bex_Un: "(∃x ∈ A∪B. P(x)) <-> (∃x ∈ A. P(x)) | (∃x ∈ B. P(x))";
      by blast

    lemma ball_UN: "(∀z ∈ (\<Union>x∈A. B(x)). P(z)) <-> (∀x∈A. ∀z ∈ B(x). P(z))"
      by blast

    lemma bex_UN: "(∃z ∈ (\<Union>x∈A. B(x)). P(z)) <-> (∃x∈A. ∃z∈B(x). P(z))"
      by blast

    subsection{*Converse of a Relation*}

    lemma converse_iff [simp]: "<a,b>∈ converse(r) <-> <b,a>∈r"
    by (unfold converse_def, blast)

    lemma converseI [intro!]: "<a,b>∈r ==> <b,a>∈converse(r)"
    by (unfold converse_def, blast)

    lemma converseD: "<a,b> ∈ converse(r) ==> <b,a> ∈ r"
    by (unfold converse_def, blast)

    lemma converseE [elim!]:
        "[| yx ∈ converse(r);
            !!x y. [| yx=<y,x>;  <x,y>∈r |] ==> P |]
         ==> P"
    by (unfold converse_def, blast)

    lemma converse_converse: "r⊆Sigma(A,B) ==> converse(converse(r)) = r"
    by blast

    lemma converse_type: "r⊆A*B ==> converse(r)⊆B*A"
    by blast

    lemma converse_prod [simp]: "converse(A*B) = B*A"
    by blast

    lemma converse_empty [simp]: "converse(0) = 0"
    by blast

    lemma converse_subset_iff:
         "A ⊆ Sigma(X,Y) ==> converse(A) ⊆ converse(B) <-> A ⊆ B"
    by blast

    subsection{*Finite Set Constructions Using @{term cons}*}

    lemma cons_subsetI: "[| a∈C; B⊆C |] ==> cons(a,B) ⊆ C"
    by blast

    lemma subset_consI: "B ⊆ cons(a,B)"
    by blast

    lemma cons_subset_iff [iff]: "cons(a,B)⊆C <-> a∈C & B⊆C"
    by blast

    (*A safe special case of subset elimination, adding no new variables
      [| cons(a,B) ⊆ C; [| a ∈ C; B ⊆ C |] ==> R |] ==> R *)
    lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]

    lemma subset_empty_iff: "A⊆0 <-> A=0"
    by blast

    lemma subset_cons_iff: "C⊆cons(a,B) <-> C⊆B | (a∈C & C-{a} ⊆ B)"
    by blast

    (* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
    lemma cons_eq: "{a} Un B = cons(a,B)"
    by blast

    lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))"
    by blast

    lemma cons_absorb: "a: B ==> cons(a,B) = B"
    by blast

    lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B"
    by blast

    lemma Diff_cons_eq: "cons(a,B) - C = (if a∈C then B-C else cons(a,B-C))"
    by auto

    lemma equal_singleton [rule_format]: "[| a: C;  ∀y∈C. y=b |] ==> C = {b}"
    by blast

    lemma [simp]: "cons(a,cons(a,B)) = cons(a,B)"
    by blast

    (** singletons **)

    lemma singleton_subsetI: "a∈C ==> {a} ⊆ C"
    by blast

    lemma singleton_subsetD: "{a} ⊆ C  ==>  a∈C"
    by blast

    (** succ **)

    lemma subset_succI: "i ⊆ succ(i)"
    by blast

    (*But if j is an ordinal or is transitive, then i∈j implies i⊆j!
      See ordinal/Ord_succ_subsetI*)
    lemma succ_subsetI: "[| i∈j;  i⊆j |] ==> succ(i)⊆j"
    by (unfold succ_def, blast)

    lemma succ_subsetE:
        "[| succ(i) ⊆ j;  [| i∈j;  i⊆j |] ==> P |] ==> P"
    by (unfold succ_def, blast)

    lemma succ_subset_iff: "succ(a) ⊆ B <-> (a ⊆ B & a ∈ B)"
    by (unfold succ_def, blast)

    subsection{*Binary Intersection*}

    (** Intersection is the greatest lower bound of two sets **)

    lemma Int_subset_iff: "C ⊆ A Int B <-> C ⊆ A & C ⊆ B"
    by blast

    lemma Int_lower1: "A Int B ⊆ A"
    by blast

    lemma Int_lower2: "A Int B ⊆ B"
    by blast

    lemma Int_greatest: "[| C⊆A;  C⊆B |] ==> C ⊆ A Int B"
    by blast

    lemma Int_cons: "cons(a,B) Int C ⊆ cons(a, B Int C)"
    by blast

    lemma Int_absorb [simp]: "A Int A = A"
    by blast

    lemma Int_left_absorb: "A Int (A Int B) = A Int B"
    by blast

    lemma Int_commute: "A Int B = B Int A"
    by blast

    lemma Int_left_commute: "A Int (B Int C) = B Int (A Int C)"
    by blast

    lemma Int_assoc: "(A Int B) Int C  =  A Int (B Int C)"
    by blast

    (*Intersection is an AC-operator*)
    lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute

    lemma Int_absorb1: "B ⊆ A ==> A ∩ B = B"
      by blast

    lemma Int_absorb2: "A ⊆ B ==> A ∩ B = A"
      by blast

    lemma Int_Un_distrib: "A Int (B Un C) = (A Int B) Un (A Int C)"
    by blast

    lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)"
    by blast

    lemma subset_Int_iff: "A⊆B <-> A Int B = A"
    by (blast elim!: equalityE)

    lemma subset_Int_iff2: "A⊆B <-> B Int A = A"
    by (blast elim!: equalityE)

    lemma Int_Diff_eq: "C⊆A ==> (A-B) Int C = C-B"
    by blast

    lemma Int_cons_left:
         "cons(a,A) Int B = (if a ∈ B then cons(a, A Int B) else A Int B)"
    by auto

    lemma Int_cons_right:
         "A Int cons(a, B) = (if a ∈ A then cons(a, A Int B) else A Int B)"
    by auto

    lemma cons_Int_distrib: "cons(x, A ∩ B) = cons(x, A) ∩ cons(x, B)"
    by auto

    subsection{*Binary Union*}

    (** Union is the least upper bound of two sets *)

    lemma Un_subset_iff: "A Un B ⊆ C <-> A ⊆ C & B ⊆ C"
    by blast

    lemma Un_upper1: "A ⊆ A Un B"
    by blast

    lemma Un_upper2: "B ⊆ A Un B"
    by blast

    lemma Un_least: "[| A⊆C;  B⊆C |] ==> A Un B ⊆ C"
    by blast

    lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)"
    by blast

    lemma Un_absorb [simp]: "A Un A = A"
    by blast

    lemma Un_left_absorb: "A Un (A Un B) = A Un B"
    by blast

    lemma Un_commute: "A Un B = B Un A"
    by blast

    lemma Un_left_commute: "A Un (B Un C) = B Un (A Un C)"
    by blast

    lemma Un_assoc: "(A Un B) Un C  =  A Un (B Un C)"
    by blast

    (*Union is an AC-operator*)
    lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute

    lemma Un_absorb1: "A ⊆ B ==> A ∪ B = B"
      by blast

    lemma Un_absorb2: "B ⊆ A ==> A ∪ B = A"
      by blast

    lemma Un_Int_distrib: "(A Int B) Un C  =  (A Un C) Int (B Un C)"
    by blast

    lemma subset_Un_iff: "A⊆B <-> A Un B = B"
    by (blast elim!: equalityE)

    lemma subset_Un_iff2: "A⊆B <-> B Un A = B"
    by (blast elim!: equalityE)

    lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)"
    by blast

    lemma Un_eq_Union: "A Un B = Union({A, B})"
    by blast

    subsection{*Set Difference*}

    lemma Diff_subset: "A-B ⊆ A"
    by blast

    lemma Diff_contains: "[| C⊆A;  C Int B = 0 |] ==> C ⊆ A-B"
    by blast

    lemma subset_Diff_cons_iff: "B ⊆ A - cons(c,C)  <->  B⊆A-C & c ~: B"
    by blast

    lemma Diff_cancel: "A - A = 0"
    by blast

    lemma Diff_triv: "A  Int B = 0 ==> A - B = A"
    by blast

    lemma empty_Diff [simp]: "0 - A = 0"
    by blast

    lemma Diff_0 [simp]: "A - 0 = A"
    by blast

    lemma Diff_eq_0_iff: "A - B = 0 <-> A ⊆ B"
    by (blast elim: equalityE)

    (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
    lemma Diff_cons: "A - cons(a,B) = A - B - {a}"
    by blast

    (*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*)
    lemma Diff_cons2: "A - cons(a,B) = A - {a} - B"
    by blast

    lemma Diff_disjoint: "A Int (B-A) = 0"
    by blast

    lemma Diff_partition: "A⊆B ==> A Un (B-A) = B"
    by blast

    lemma subset_Un_Diff: "A ⊆ B Un (A - B)"
    by blast

    lemma double_complement: "[| A⊆B; B⊆C |] ==> B-(C-A) = A"
    by blast

    lemma double_complement_Un: "(A Un B) - (B-A) = A"
    by blast

    lemma Un_Int_crazy:
     "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)"
    apply blast
    done

    lemma Diff_Un: "A - (B Un C) = (A-B) Int (A-C)"
    by blast

    lemma Diff_Int: "A - (B Int C) = (A-B) Un (A-C)"
    by blast

    lemma Un_Diff: "(A Un B) - C = (A - C) Un (B - C)"
    by blast

    lemma Int_Diff: "(A Int B) - C = A Int (B - C)"
    by blast

    lemma Diff_Int_distrib: "C Int (A-B) = (C Int A) - (C Int B)"
    by blast

    lemma Diff_Int_distrib2: "(A-B) Int C = (A Int C) - (B Int C)"
    by blast

    (*Halmos, Naive Set Theory, page 16.*)
    lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C)  <->  C⊆A"
    by (blast elim!: equalityE)

    subsection{*Big Union and Intersection*}

    (** Big Union is the least upper bound of a set  **)

    lemma Union_subset_iff: "Union(A) ⊆ C <-> (∀x∈A. x ⊆ C)"
    by blast

    lemma Union_upper: "B∈A ==> B ⊆ Union(A)"
    by blast

    lemma Union_least: "[| !!x. x∈A ==> x⊆C |] ==> Union(A) ⊆ C"
    by blast

    lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)"
    by blast

    lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)"
    by blast

    lemma Union_Int_subset: "Union(A Int B) ⊆ Union(A) Int Union(B)"
    by blast

    lemma Union_disjoint: "Union(C) Int A = 0 <-> (∀B∈C. B Int A = 0)"
    by (blast elim!: equalityE)

    lemma Union_empty_iff: "Union(A) = 0 <-> (∀B∈A. B=0)"
    by blast

    lemma Int_Union2: "Union(B) Int A = (\<Union>C∈B. C Int A)"
    by blast

    (** Big Intersection is the greatest lower bound of a nonempty set **)

    lemma Inter_subset_iff: "A≠0  ==>  C ⊆ Inter(A) <-> (∀x∈A. C ⊆ x)"
    by blast

    lemma Inter_lower: "B∈A ==> Inter(A) ⊆ B"
    by blast

    lemma Inter_greatest: "[| A≠0;  !!x. x∈A ==> C⊆x |] ==> C ⊆ Inter(A)"
    by blast

    (** Intersection of a family of sets  **)

    lemma INT_lower: "x∈A ==> (\<Inter>x∈A. B(x)) ⊆ B(x)"
    by blast

    lemma INT_greatest: "[| A≠0;  !!x. x∈A ==> C⊆B(x) |] ==> C ⊆ (\<Inter>x∈A. B(x))"
    by force

    lemma Inter_0 [simp]: "Inter(0) = 0"
    by (unfold Inter_def, blast)

    lemma Inter_Un_subset:
         "[| z∈A; z∈B |] ==> Inter(A) Un Inter(B) ⊆ Inter(A Int B)"
    by blast

    (* A good challenge: Inter is ill-behaved on the empty set *)
    lemma Inter_Un_distrib:
         "[| A≠0;  B≠0 |] ==> Inter(A Un B) = Inter(A) Int Inter(B)"
    by blast

    lemma Union_singleton: "Union({b}) = b"
    by blast

    lemma Inter_singleton: "Inter({b}) = b"
    by blast

    lemma Inter_cons [simp]:
         "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))"
    by force

    subsection{*Unions and Intersections of Families*}

    lemma subset_UN_iff_eq: "A ⊆ (\<Union>i∈I. B(i)) <-> A = (\<Union>i∈I. A Int B(i))"
    by (blast elim!: equalityE)

    lemma UN_subset_iff: "(\<Union>x∈A. B(x)) ⊆ C <-> (∀x∈A. B(x) ⊆ C)"
    by blast

    lemma UN_upper: "x∈A ==> B(x) ⊆ (\<Union>x∈A. B(x))"
    by (erule RepFunI [THEN Union_upper])

    lemma UN_least: "[| !!x. x∈A ==> B(x)⊆C |] ==> (\<Union>x∈A. B(x)) ⊆ C"
    by blast

    lemma Union_eq_UN: "Union(A) = (\<Union>x∈A. x)"
    by blast

    lemma Inter_eq_INT: "Inter(A) = (\<Inter>x∈A. x)"
    by (unfold Inter_def, blast)

    lemma UN_0 [simp]: "(\<Union>i∈0. A(i)) = 0"
    by blast

    lemma UN_singleton: "(\<Union>x∈A. {x}) = A"
    by blast

    lemma UN_Un: "(\<Union>i∈ A Un B. C(i)) = (\<Union>i∈ A. C(i)) Un (\<Union>i∈B. C(i))"
    by blast

    lemma INT_Un: "(\<Inter>i∈I Un J. A(i)) =
                   (if I=0 then \<Inter>j∈J. A(j)
                           else if J=0 then \<Inter>i∈I. A(i)
                           else ((\<Inter>i∈I. A(i)) Int  (\<Inter>j∈J. A(j))))"
    by (simp, blast intro!: equalityI)

    lemma UN_UN_flatten: "(\<Union>x ∈ (\<Union>y∈A. B(y)). C(x)) = (\<Union>y∈A. \<Union>x∈ B(y). C(x))"
    by blast

    (*Halmos, Naive Set Theory, page 35.*)
    lemma Int_UN_distrib: "B Int (\<Union>i∈I. A(i)) = (\<Union>i∈I. B Int A(i))"
    by blast

    lemma Un_INT_distrib: "I≠0 ==> B Un (\<Inter>i∈I. A(i)) = (\<Inter>i∈I. B Un A(i))"
    by auto

    lemma Int_UN_distrib2:
         "(\<Union>i∈I. A(i)) Int (\<Union>j∈J. B(j)) = (\<Union>i∈I. \<Union>j∈J. A(i) Int B(j))"
    by blast

    lemma Un_INT_distrib2: "[| I≠0;  J≠0 |] ==>
          (\<Inter>i∈I. A(i)) Un (\<Inter>j∈J. B(j)) = (\<Inter>i∈I. \<Inter>j∈J. A(i) Un B(j))"
    by auto

    lemma UN_constant [simp]: "(\<Union>y∈A. c) = (if A=0 then 0 else c)"
    by force

    lemma INT_constant [simp]: "(\<Inter>y∈A. c) = (if A=0 then 0 else c)"
    by force

    lemma UN_RepFun [simp]: "(\<Union>y∈ RepFun(A,f). B(y)) = (\<Union>x∈A. B(f(x)))"
    by blast

    lemma INT_RepFun [simp]: "(\<Inter>x∈RepFun(A,f). B(x))    = (\<Inter>a∈A. B(f(a)))"
    by (auto simp add: Inter_def)

    lemma INT_Union_eq:
         "0 ~: A ==> (\<Inter>x∈ Union(A). B(x)) = (\<Inter>y∈A. \<Inter>x∈y. B(x))"
    apply (subgoal_tac "∀x∈A. x~=0")
     prefer 2 apply blast
    apply (force simp add: Inter_def ball_conj_distrib)
    done

    lemma INT_UN_eq:
         "(∀x∈A. B(x) ~= 0)
          ==> (\<Inter>z∈ (\<Union>x∈A. B(x)). C(z)) = (\<Inter>x∈A. \<Inter>z∈ B(x). C(z))"
    apply (subst INT_Union_eq, blast)
    apply (simp add: Inter_def)
    done

    (** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
        Union of a family of unions **)

    lemma UN_Un_distrib:
         "(\<Union>i∈I. A(i) Un B(i)) = (\<Union>i∈I. A(i))  Un  (\<Union>i∈I. B(i))"
    by blast

    lemma INT_Int_distrib:
         "I≠0 ==> (\<Inter>i∈I. A(i) Int B(i)) = (\<Inter>i∈I. A(i)) Int (\<Inter>i∈I. B(i))"
    by (blast elim!: not_emptyE)

    lemma UN_Int_subset:
         "(\<Union>z∈I Int J. A(z)) ⊆ (\<Union>z∈I. A(z)) Int (\<Union>z∈J. A(z))"
    by blast

    (** Devlin, page 12, exercise 5: Complements **)

    lemma Diff_UN: "I≠0 ==> B - (\<Union>i∈I. A(i)) = (\<Inter>i∈I. B - A(i))"
    by (blast elim!: not_emptyE)

    lemma Diff_INT: "I≠0 ==> B - (\<Inter>i∈I. A(i)) = (\<Union>i∈I. B - A(i))"
    by (blast elim!: not_emptyE)

    (** Unions and Intersections with General Sum **)

    (*Not suitable for rewriting: LOOPS!*)
    lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)"
    by blast

    (*Not suitable for rewriting: LOOPS!*)
    lemma Sigma_cons2: "A * cons(b,B) = A*{b} Un A*B"
    by blast

    lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)"
    by blast

    lemma Sigma_succ2: "A * succ(B) = A*{B} Un A*B"
    by blast

    lemma SUM_UN_distrib1:
         "(Σ x ∈ (\<Union>y∈A. C(y)). B(x)) = (\<Union>y∈A. Σ x∈C(y). B(x))"
    by blast

    lemma SUM_UN_distrib2:
         "(Σ i∈I. \<Union>j∈J. C(i,j)) = (\<Union>j∈J. Σ i∈I. C(i,j))"
    by blast

    lemma SUM_Un_distrib1:
         "(Σ i∈I Un J. C(i)) = (Σ i∈I. C(i)) Un (Σ j∈J. C(j))"
    by blast

    lemma SUM_Un_distrib2:
         "(Σ i∈I. A(i) Un B(i)) = (Σ i∈I. A(i)) Un (Σ i∈I. B(i))"
    by blast

    (*First-order version of the above, for rewriting*)
    lemma prod_Un_distrib2: "I * (A Un B) = I*A Un I*B"
    by (rule SUM_Un_distrib2)

    lemma SUM_Int_distrib1:
         "(Σ i∈I Int J. C(i)) = (Σ i∈I. C(i)) Int (Σ j∈J. C(j))"
    by blast

    lemma SUM_Int_distrib2:
         "(Σ i∈I. A(i) Int B(i)) = (Σ i∈I. A(i)) Int (Σ i∈I. B(i))"
    by blast

    (*First-order version of the above, for rewriting*)
    lemma prod_Int_distrib2: "I * (A Int B) = I*A Int I*B"
    by (rule SUM_Int_distrib2)

    (*Cf Aczel, Non-Well-Founded Sets, page 115*)
    lemma SUM_eq_UN: "(Σ i∈I. A(i)) = (\<Union>i∈I. {i} * A(i))"
    by blast

    lemma times_subset_iff:
         "(A'*B' ⊆ A*B) <-> (A' = 0 | B' = 0 | (A'⊆A) & (B'⊆B))"
    by blast

    lemma Int_Sigma_eq:
         "(Σ x ∈ A'. B'(x)) Int (Σ x ∈ A. B(x)) = (Σ x ∈ A' Int A. B'(x) Int B(x))"
    by blast

    (** Domain **)

    lemma domain_iff: "a: domain(r) <-> (EX y. <a,y>∈ r)"
    by (unfold domain_def, blast)

    lemma domainI [intro]: "<a,b>∈ r ==> a: domain(r)"
    by (unfold domain_def, blast)

    lemma domainE [elim!]:
        "[| a ∈ domain(r);  !!y. <a,y>∈ r ==> P |] ==> P"
    by (unfold domain_def, blast)

    lemma domain_subset: "domain(Sigma(A,B)) ⊆ A"
    by blast

    lemma domain_of_prod: "b∈B ==> domain(A*B) = A"
    by blast

    lemma domain_0 [simp]: "domain(0) = 0"
    by blast

    lemma domain_cons [simp]: "domain(cons(<a,b>,r)) = cons(a, domain(r))"
    by blast

    lemma domain_Un_eq [simp]: "domain(A Un B) = domain(A) Un domain(B)"
    by blast

    lemma domain_Int_subset: "domain(A Int B) ⊆ domain(A) Int domain(B)"
    by blast

    lemma domain_Diff_subset: "domain(A) - domain(B) ⊆ domain(A - B)"
    by blast

    lemma domain_UN: "domain(\<Union>x∈A. B(x)) = (\<Union>x∈A. domain(B(x)))"
    by blast

    lemma domain_Union: "domain(Union(A)) = (\<Union>x∈A. domain(x))"
    by blast

    (** Range **)

    lemma rangeI [intro]: "<a,b>∈ r ==> b ∈ range(r)"
    apply (unfold range_def)
    apply (erule converseI [THEN domainI])
    done

    lemma rangeE [elim!]: "[| b ∈ range(r);  !!x. <x,b>∈ r ==> P |] ==> P"
    by (unfold range_def, blast)

    lemma range_subset: "range(A*B) ⊆ B"
    apply (unfold range_def)
    apply (subst converse_prod)
    apply (rule domain_subset)
    done

    lemma range_of_prod: "a∈A ==> range(A*B) = B"
    by blast

    lemma range_0 [simp]: "range(0) = 0"
    by blast

    lemma range_cons [simp]: "range(cons(<a,b>,r)) = cons(b, range(r))"
    by blast

    lemma range_Un_eq [simp]: "range(A Un B) = range(A) Un range(B)"
    by blast

    lemma range_Int_subset: "range(A Int B) ⊆ range(A) Int range(B)"
    by blast

    lemma range_Diff_subset: "range(A) - range(B) ⊆ range(A - B)"
    by blast

    lemma domain_converse [simp]: "domain(converse(r)) = range(r)"
    by blast

    lemma range_converse [simp]: "range(converse(r)) = domain(r)"
    by blast

    (** Field **)

    lemma fieldI1: "<a,b>∈ r ==> a ∈ field(r)"
    by (unfold field_def, blast)

    lemma fieldI2: "<a,b>∈ r ==> b ∈ field(r)"
    by (unfold field_def, blast)

    lemma fieldCI [intro]:
        "(~ <c,a>∈r ==> <a,b>∈ r) ==> a ∈ field(r)"
    apply (unfold field_def, blast)
    done

    lemma fieldE [elim!]:
         "[| a ∈ field(r);
             !!x. <a,x>∈ r ==> P;
             !!x. <x,a>∈ r ==> P        |] ==> P"
    by (unfold field_def, blast)

    lemma field_subset: "field(A*B) ⊆ A Un B"
    by blast

    lemma domain_subset_field: "domain(r) ⊆ field(r)"
    apply (unfold field_def)
    apply (rule Un_upper1)
    done

    lemma range_subset_field: "range(r) ⊆ field(r)"
    apply (unfold field_def)
    apply (rule Un_upper2)
    done

    lemma domain_times_range: "r ⊆ Sigma(A,B) ==> r ⊆ domain(r)*range(r)"
    by blast

    lemma field_times_field: "r ⊆ Sigma(A,B) ==> r ⊆ field(r)*field(r)"
    by blast

    lemma relation_field_times_field: "relation(r) ==> r ⊆ field(r)*field(r)"
    by (simp add: relation_def, blast)

    lemma field_of_prod: "field(A*A) = A"
    by blast

    lemma field_0 [simp]: "field(0) = 0"
    by blast

    lemma field_cons [simp]: "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
    by blast

    lemma field_Un_eq [simp]: "field(A Un B) = field(A) Un field(B)"
    by blast

    lemma field_Int_subset: "field(A Int B) ⊆ field(A) Int field(B)"
    by blast

    lemma field_Diff_subset: "field(A) - field(B) ⊆ field(A - B)"
    by blast

    lemma field_converse [simp]: "field(converse(r)) = field(r)"
    by blast

    (** The Union of a set of relations is a relation -- Lemma for fun_Union **)
    lemma rel_Union: "(∀x∈S. EX A B. x ⊆ A*B) ==>
                      Union(S) ⊆ domain(Union(S)) * range(Union(S))"
    by blast

    (** The Union of 2 relations is a relation (Lemma for fun_Un)  **)
    lemma rel_Un: "[| r ⊆ A*B;  s ⊆ C*D |] ==> (r Un s) ⊆ (A Un C) * (B Un D)"
    by blast

    lemma domain_Diff_eq: "[| <a,c> ∈ r; c~=b |] ==> domain(r-{<a,b>}) = domain(r)"
    by blast

    lemma range_Diff_eq: "[| <c,b> ∈ r; c~=a |] ==> range(r-{<a,b>}) = range(r)"
    by blast

    subsection{*Image of a Set under a Function or Relation*}

    lemma image_iff: "b ∈ r``A <-> (∃x∈A. <x,b>∈r)"
    by (unfold image_def, blast)

    lemma image_singleton_iff: "b ∈ r``{a} <-> <a,b>∈r"
    by (rule image_iff [THEN iff_trans], blast)

    lemma imageI [intro]: "[| <a,b>∈ r;  a∈A |] ==> b ∈ r``A"
    by (unfold image_def, blast)

    lemma imageE [elim!]:
        "[| b: r``A;  !!x.[| <x,b>∈ r;  x∈A |] ==> P |] ==> P"
    by (unfold image_def, blast)

    lemma image_subset: "r ⊆ A*B ==> r``C ⊆ B"
    by blast

    lemma image_0 [simp]: "r``0 = 0"
    by blast

    lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)"
    by blast

    lemma image_UN: "r `` (\<Union>x∈A. B(x)) = (\<Union>x∈A. r `` B(x))"
    by blast

    lemma Collect_image_eq:
         "{z ∈ Sigma(A,B). P(z)} `` C = (\<Union>x ∈ A. {y ∈ B(x). x ∈ C & P(<x,y>)})"
    by blast

    lemma image_Int_subset: "r``(A Int B) ⊆ (r``A) Int (r``B)"
    by blast

    lemma image_Int_square_subset: "(r Int A*A)``B ⊆ (r``B) Int A"
    by blast

    lemma image_Int_square: "B⊆A ==> (r Int A*A)``B = (r``B) Int A"
    by blast

    (*Image laws for special relations*)
    lemma image_0_left [simp]: "0``A = 0"
    by blast

    lemma image_Un_left: "(r Un s)``A = (r``A) Un (s``A)"
    by blast

    lemma image_Int_subset_left: "(r Int s)``A ⊆ (r``A) Int (s``A)"
    by blast

    subsection{*Inverse Image of a Set under a Function or Relation*}

    lemma vimage_iff:
        "a ∈ r-``B <-> (∃y∈B. <a,y>∈r)"
    by (unfold vimage_def image_def converse_def, blast)

    lemma vimage_singleton_iff: "a ∈ r-``{b} <-> <a,b>∈r"
    by (rule vimage_iff [THEN iff_trans], blast)

    lemma vimageI [intro]: "[| <a,b>∈ r;  b∈B |] ==> a ∈ r-``B"
    by (unfold vimage_def, blast)

    lemma vimageE [elim!]:
        "[| a: r-``B;  !!x.[| <a,x>∈ r;  x∈B |] ==> P |] ==> P"
    apply (unfold vimage_def, blast)
    done

    lemma vimage_subset: "r ⊆ A*B ==> r-``C ⊆ A"
    apply (unfold vimage_def)
    apply (erule converse_type [THEN image_subset])
    done

    lemma vimage_0 [simp]: "r-``0 = 0"
    by blast

    lemma vimage_Un [simp]: "r-``(A Un B) = (r-``A) Un (r-``B)"
    by blast

    lemma vimage_Int_subset: "r-``(A Int B) ⊆ (r-``A) Int (r-``B)"
    by blast

    (*NOT suitable for rewriting*)
    lemma vimage_eq_UN: "f -``B = (\<Union>y∈B. f-``{y})"
    by blast

    lemma function_vimage_Int:
         "function(f) ==> f-``(A Int B) = (f-``A)  Int  (f-``B)"
    by (unfold function_def, blast)

    lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)"
    by (unfold function_def, blast)

    lemma function_image_vimage: "function(f) ==> f `` (f-`` A) ⊆ A"
    by (unfold function_def, blast)

    lemma vimage_Int_square_subset: "(r Int A*A)-``B ⊆ (r-``B) Int A"
    by blast

    lemma vimage_Int_square: "B⊆A ==> (r Int A*A)-``B = (r-``B) Int A"
    by blast

    (*Invese image laws for special relations*)
    lemma vimage_0_left [simp]: "0-``A = 0"
    by blast

    lemma vimage_Un_left: "(r Un s)-``A = (r-``A) Un (s-``A)"
    by blast

    lemma vimage_Int_subset_left: "(r Int s)-``A ⊆ (r-``A) Int (s-``A)"
    by blast

    (** Converse **)

    lemma converse_Un [simp]: "converse(A Un B) = converse(A) Un converse(B)"
    by blast

    lemma converse_Int [simp]: "converse(A Int B) = converse(A) Int converse(B)"
    by blast

    lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)"
    by blast

    lemma converse_UN [simp]: "converse(\<Union>x∈A. B(x)) = (\<Union>x∈A. converse(B(x)))"
    by blast

    (*Unfolding Inter avoids using excluded middle on A=0*)
    lemma converse_INT [simp]:
         "converse(\<Inter>x∈A. B(x)) = (\<Inter>x∈A. converse(B(x)))"
    apply (unfold Inter_def, blast)
    done

    subsection{*Powerset Operator*}

    lemma Pow_0 [simp]: "Pow(0) = {0}"
    by blast

    lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}"
    apply (rule equalityI, safe)
    apply (erule swap)
    apply (rule_tac a = "x-{a}" in RepFun_eqI, auto)
    done

    lemma Un_Pow_subset: "Pow(A) Un Pow(B) ⊆ Pow(A Un B)"
    by blast

    lemma UN_Pow_subset: "(\<Union>x∈A. Pow(B(x))) ⊆ Pow(\<Union>x∈A. B(x))"
    by blast

    lemma subset_Pow_Union: "A ⊆ Pow(Union(A))"
    by blast

    lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A"
    by blast

    lemma Union_Pow_iff: "Union(A) ∈ Pow(B) <-> A ∈ Pow(Pow(B))"
    by blast

    lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)"
    by blast

    lemma Pow_INT_eq: "A≠0 ==> Pow(\<Inter>x∈A. B(x)) = (\<Inter>x∈A. Pow(B(x)))"
    by (blast elim!: not_emptyE)

    subsection{*RepFun*}

    lemma RepFun_subset: "[| !!x. x∈A ==> f(x) ∈ B |] ==> {f(x). x∈A} ⊆ B"
    by blast

    lemma RepFun_eq_0_iff [simp]: "{f(x).x∈A}=0 <-> A=0"
    by blast

    lemma RepFun_constant [simp]: "{c. x∈A} = (if A=0 then 0 else {c})"
    by force

    subsection{*Collect*}

    lemma Collect_subset: "Collect(A,P) ⊆ A"
    by blast

    lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)"
    by blast

    lemma Collect_Int: "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)"
    by blast

    lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)"
    by blast

    lemma Collect_cons: "{x∈cons(a,B). P(x)} =
          (if P(a) then cons(a, {x∈B. P(x)}) else {x∈B. P(x)})"
    by (simp, blast)

    lemma Int_Collect_self_eq: "A Int Collect(A,P) = Collect(A,P)"
    by blast

    lemma Collect_Collect_eq [simp]:
         "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))"
    by blast

    lemma Collect_Int_Collect_eq:
         "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))"
    by blast

    lemma Collect_Union_eq [simp]:
         "Collect(\<Union>x∈A. B(x), P) = (\<Union>x∈A. Collect(B(x), P))"
    by blast

    lemma Collect_Int_left: "{x∈A. P(x)} Int B = {x ∈ A Int B. P(x)}"
    by blast

    lemma Collect_Int_right: "A Int {x∈B. P(x)} = {x ∈ A Int B. P(x)}"
    by blast

    lemma Collect_disj_eq: "{x∈A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
    by blast

    lemma Collect_conj_eq: "{x∈A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
    by blast

    lemmas subset_SIs = subset_refl cons_subsetI subset_consI
                        Union_least UN_least Un_least
                        Inter_greatest Int_greatest RepFun_subset
                        Un_upper1 Un_upper2 Int_lower1 Int_lower2

    (*First, ML bindings from the old file subset.ML*)
    ML
    {*
    val cons_subsetI = thm "cons_subsetI";
    val subset_consI = thm "subset_consI";
    val cons_subset_iff = thm "cons_subset_iff";
    val cons_subsetE = thm "cons_subsetE";
    val subset_empty_iff = thm "subset_empty_iff";
    val subset_cons_iff = thm "subset_cons_iff";
    val subset_succI = thm "subset_succI";
    val succ_subsetI = thm "succ_subsetI";
    val succ_subsetE = thm "succ_subsetE";
    val succ_subset_iff = thm "succ_subset_iff";
    val singleton_subsetI = thm "singleton_subsetI";
    val singleton_subsetD = thm "singleton_subsetD";
    val Union_subset_iff = thm "Union_subset_iff";
    val Union_upper = thm "Union_upper";
    val Union_least = thm "Union_least";
    val subset_UN_iff_eq = thm "subset_UN_iff_eq";
    val UN_subset_iff = thm "UN_subset_iff";
    val UN_upper = thm "UN_upper";
    val UN_least = thm "UN_least";
    val Inter_subset_iff = thm "Inter_subset_iff";
    val Inter_lower = thm "Inter_lower";
    val Inter_greatest = thm "Inter_greatest";
    val INT_lower = thm "INT_lower";
    val INT_greatest = thm "INT_greatest";
    val Un_subset_iff = thm "Un_subset_iff";
    val Un_upper1 = thm "Un_upper1";
    val Un_upper2 = thm "Un_upper2";
    val Un_least = thm "Un_least";
    val Int_subset_iff = thm "Int_subset_iff";
    val Int_lower1 = thm "Int_lower1";
    val Int_lower2 = thm "Int_lower2";
    val Int_greatest = thm "Int_greatest";
    val Diff_subset = thm "Diff_subset";
    val Diff_contains = thm "Diff_contains";
    val subset_Diff_cons_iff = thm "subset_Diff_cons_iff";
    val Collect_subset = thm "Collect_subset";
    val RepFun_subset = thm "RepFun_subset";

    val subset_SIs = thms "subset_SIs";

    val subset_cs = claset()
        delrules [subsetI, subsetCE]
        addSIs subset_SIs
        addIs  [Union_upper, Inter_lower]
        addSEs [cons_subsetE];
    *}
    (*subset_cs is a claset for subset reasoning*)

    ML
    {*
    val ZF_cs = claset() delrules [equalityI];

    val in_mono = thm "in_mono";
    val conj_mono = thm "conj_mono";
    val disj_mono = thm "disj_mono";
    val imp_mono = thm "imp_mono";
    val imp_refl = thm "imp_refl";
    val ex_mono = thm "ex_mono";
    val all_mono = thm "all_mono";

    val converse_iff = thm "converse_iff";
    val converseI = thm "converseI";
    val converseD = thm "converseD";
    val converseE = thm "converseE";
    val converse_converse = thm "converse_converse";
    val converse_type = thm "converse_type";
    val converse_prod = thm "converse_prod";
    val converse_empty = thm "converse_empty";
    val converse_subset_iff = thm "converse_subset_iff";
    val domain_iff = thm "domain_iff";
    val domainI = thm "domainI";
    val domainE = thm "domainE";
    val domain_subset = thm "domain_subset";
    val rangeI = thm "rangeI";
    val rangeE = thm "rangeE";
    val range_subset = thm "range_subset";
    val fieldI1 = thm "fieldI1";
    val fieldI2 = thm "fieldI2";
    val fieldCI = thm "fieldCI";
    val fieldE = thm "fieldE";
    val field_subset = thm "field_subset";
    val domain_subset_field = thm "domain_subset_field";
    val range_subset_field = thm "range_subset_field";
    val domain_times_range = thm "domain_times_range";
    val field_times_field = thm "field_times_field";
    val image_iff = thm "image_iff";
    val image_singleton_iff = thm "image_singleton_iff";
    val imageI = thm "imageI";
    val imageE = thm "imageE";
    val image_subset = thm "image_subset";
    val vimage_iff = thm "vimage_iff";
    val vimage_singleton_iff = thm "vimage_singleton_iff";
    val vimageI = thm "vimageI";
    val vimageE = thm "vimageE";
    val vimage_subset = thm "vimage_subset";
    val rel_Union = thm "rel_Union";
    val rel_Un = thm "rel_Un";
    val domain_Diff_eq = thm "domain_Diff_eq";
    val range_Diff_eq = thm "range_Diff_eq";
    val cons_eq = thm "cons_eq";
    val cons_commute = thm "cons_commute";
    val cons_absorb = thm "cons_absorb";
    val cons_Diff = thm "cons_Diff";
    val equal_singleton = thm "equal_singleton";
    val Int_cons = thm "Int_cons";
    val Int_absorb = thm "Int_absorb";
    val Int_left_absorb = thm "Int_left_absorb";
    val Int_commute = thm "Int_commute";
    val Int_left_commute = thm "Int_left_commute";
    val Int_assoc = thm "Int_assoc";
    val Int_Un_distrib = thm "Int_Un_distrib";
    val Int_Un_distrib2 = thm "Int_Un_distrib2";
    val subset_Int_iff = thm "subset_Int_iff";
    val subset_Int_iff2 = thm "subset_Int_iff2";
    val Int_Diff_eq = thm "Int_Diff_eq";
    val Int_cons_left = thm "Int_cons_left";
    val Int_cons_right = thm "Int_cons_right";
    val Un_cons = thm "Un_cons";
    val Un_absorb = thm "Un_absorb";
    val Un_left_absorb = thm "Un_left_absorb";
    val Un_commute = thm "Un_commute";
    val Un_left_commute = thm "Un_left_commute";
    val Un_assoc = thm "Un_assoc";
    val Un_Int_distrib = thm "Un_Int_distrib";
    val subset_Un_iff = thm "subset_Un_iff";
    val subset_Un_iff2 = thm "subset_Un_iff2";
    val Un_empty = thm "Un_empty";
    val Un_eq_Union = thm "Un_eq_Union";
    val Diff_cancel = thm "Diff_cancel";
    val Diff_triv = thm "Diff_triv";
    val empty_Diff = thm "empty_Diff";
    val Diff_0 = thm "Diff_0";
    val Diff_eq_0_iff = thm "Diff_eq_0_iff";
    val Diff_cons = thm "Diff_cons";
    val Diff_cons2 = thm "Diff_cons2";
    val Diff_disjoint = thm "Diff_disjoint";
    val Diff_partition = thm "Diff_partition";
    val subset_Un_Diff = thm "subset_Un_Diff";
    val double_complement = thm "double_complement";
    val double_complement_Un = thm "double_complement_Un";
    val Un_Int_crazy = thm "Un_Int_crazy";
    val Diff_Un = thm "Diff_Un";
    val Diff_Int = thm "Diff_Int";
    val Un_Diff = thm "Un_Diff";
    val Int_Diff = thm "Int_Diff";
    val Diff_Int_distrib = thm "Diff_Int_distrib";
    val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
    val Un_Int_assoc_iff = thm "Un_Int_assoc_iff";
    val Union_cons = thm "Union_cons";
    val Union_Un_distrib = thm "Union_Un_distrib";
    val Union_Int_subset = thm "Union_Int_subset";
    val Union_disjoint = thm "Union_disjoint";
    val Union_empty_iff = thm "Union_empty_iff";
    val Int_Union2 = thm "Int_Union2";
    val Inter_0 = thm "Inter_0";
    val Inter_Un_subset = thm "Inter_Un_subset";
    val Inter_Un_distrib = thm "Inter_Un_distrib";
    val Union_singleton = thm "Union_singleton";
    val Inter_singleton = thm "Inter_singleton";
    val Inter_cons = thm "Inter_cons";
    val Union_eq_UN = thm "Union_eq_UN";
    val Inter_eq_INT = thm "Inter_eq_INT";
    val UN_0 = thm "UN_0";
    val UN_singleton = thm "UN_singleton";
    val UN_Un = thm "UN_Un";
    val INT_Un = thm "INT_Un";
    val UN_UN_flatten = thm "UN_UN_flatten";
    val Int_UN_distrib = thm "Int_UN_distrib";
    val Un_INT_distrib = thm "Un_INT_distrib";
    val Int_UN_distrib2 = thm "Int_UN_distrib2";
    val Un_INT_distrib2 = thm "Un_INT_distrib2";
    val UN_constant = thm "UN_constant";
    val INT_constant = thm "INT_constant";
    val UN_RepFun = thm "UN_RepFun";
    val INT_RepFun = thm "INT_RepFun";
    val INT_Union_eq = thm "INT_Union_eq";
    val INT_UN_eq = thm "INT_UN_eq";
    val UN_Un_distrib = thm "UN_Un_distrib";
    val INT_Int_distrib = thm "INT_Int_distrib";
    val UN_Int_subset = thm "UN_Int_subset";
    val Diff_UN = thm "Diff_UN";
    val Diff_INT = thm "Diff_INT";
    val Sigma_cons1 = thm "Sigma_cons1";
    val Sigma_cons2 = thm "Sigma_cons2";
    val Sigma_succ1 = thm "Sigma_succ1";
    val Sigma_succ2 = thm "Sigma_succ2";
    val SUM_UN_distrib1 = thm "SUM_UN_distrib1";
    val SUM_UN_distrib2 = thm "SUM_UN_distrib2";
    val SUM_Un_distrib1 = thm "SUM_Un_distrib1";
    val SUM_Un_distrib2 = thm "SUM_Un_distrib2";
    val prod_Un_distrib2 = thm "prod_Un_distrib2";
    val SUM_Int_distrib1 = thm "SUM_Int_distrib1";
    val SUM_Int_distrib2 = thm "SUM_Int_distrib2";
    val prod_Int_distrib2 = thm "prod_Int_distrib2";
    val SUM_eq_UN = thm "SUM_eq_UN";
    val domain_of_prod = thm "domain_of_prod";
    val domain_0 = thm "domain_0";
    val domain_cons = thm "domain_cons";
    val domain_Un_eq = thm "domain_Un_eq";
    val domain_Int_subset = thm "domain_Int_subset";
    val domain_Diff_subset = thm "domain_Diff_subset";
    val domain_converse = thm "domain_converse";
    val domain_UN = thm "domain_UN";
    val domain_Union = thm "domain_Union";
    val range_of_prod = thm "range_of_prod";
    val range_0 = thm "range_0";
    val range_cons = thm "range_cons";
    val range_Un_eq = thm "range_Un_eq";
    val range_Int_subset = thm "range_Int_subset";
    val range_Diff_subset = thm "range_Diff_subset";
    val range_converse = thm "range_converse";
    val field_of_prod = thm "field_of_prod";
    val field_0 = thm "field_0";
    val field_cons = thm "field_cons";
    val field_Un_eq = thm "field_Un_eq";
    val field_Int_subset = thm "field_Int_subset";
    val field_Diff_subset = thm "field_Diff_subset";
    val field_converse = thm "field_converse";
    val image_0 = thm "image_0";
    val image_Un = thm "image_Un";
    val image_Int_subset = thm "image_Int_subset";
    val image_Int_square_subset = thm "image_Int_square_subset";
    val image_Int_square = thm "image_Int_square";
    val image_0_left = thm "image_0_left";
    val image_Un_left = thm "image_Un_left";
    val image_Int_subset_left = thm "image_Int_subset_left";
    val vimage_0 = thm "vimage_0";
    val vimage_Un = thm "vimage_Un";
    val vimage_Int_subset = thm "vimage_Int_subset";
    val vimage_eq_UN = thm "vimage_eq_UN";
    val function_vimage_Int = thm "function_vimage_Int";
    val function_vimage_Diff = thm "function_vimage_Diff";
    val function_image_vimage = thm "function_image_vimage";
    val vimage_Int_square_subset = thm "vimage_Int_square_subset";
    val vimage_Int_square = thm "vimage_Int_square";
    val vimage_0_left = thm "vimage_0_left";
    val vimage_Un_left = thm "vimage_Un_left";
    val vimage_Int_subset_left = thm "vimage_Int_subset_left";
    val converse_Un = thm "converse_Un";
    val converse_Int = thm "converse_Int";
    val converse_Diff = thm "converse_Diff";
    val converse_UN = thm "converse_UN";
    val converse_INT = thm "converse_INT";
    val Pow_0 = thm "Pow_0";
    val Pow_insert = thm "Pow_insert";
    val Un_Pow_subset = thm "Un_Pow_subset";
    val UN_Pow_subset = thm "UN_Pow_subset";
    val subset_Pow_Union = thm "subset_Pow_Union";
    val Union_Pow_eq = thm "Union_Pow_eq";
    val Union_Pow_iff = thm "Union_Pow_iff";
    val Pow_Int_eq = thm "Pow_Int_eq";
    val Pow_INT_eq = thm "Pow_INT_eq";
    val RepFun_eq_0_iff = thm "RepFun_eq_0_iff";
    val RepFun_constant = thm "RepFun_constant";
    val Collect_Un = thm "Collect_Un";
    val Collect_Int = thm "Collect_Int";
    val Collect_Diff = thm "Collect_Diff";
    val Collect_cons = thm "Collect_cons";
    val Int_Collect_self_eq = thm "Int_Collect_self_eq";
    val Collect_Collect_eq = thm "Collect_Collect_eq";
    val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq";
    val Collect_disj_eq = thm "Collect_disj_eq";
    val Collect_conj_eq = thm "Collect_conj_eq";

    val Int_ac = thms "Int_ac";
    val Un_ac = thms "Un_ac";
    val Int_absorb1 = thm "Int_absorb1";
    val Int_absorb2 = thm "Int_absorb2";
    val Un_absorb1 = thm "Un_absorb1";
    val Un_absorb2 = thm "Un_absorb2";
    *}

    end

lemma in_mono:

      A ⊆ B ==> x ∈ A --> x ∈ B

lemma the_eq_0:

      (THE x. False) = 0

### Bounded Quantifiers

lemma ball_Un:

      (∀x∈A ∪ B. P(x)) <-> (∀x∈A. P(x)) ∧ (∀x∈B. P(x))

lemma bex_Un:

      (∃x∈A ∪ B. P(x)) <-> (∃x∈A. P(x)) ∨ (∃x∈B. P(x))

lemma ball_UN:

      (∀z∈\<Union>x∈A. B(x). P(z)) <-> (∀x∈A. ∀z∈B(x). P(z))

lemma bex_UN:

      (∃z∈\<Union>x∈A. B(x). P(z)) <-> (∃x∈A. ∃z∈B(x). P(z))

### Converse of a Relation

lemma converse_iff:

      ⟨a, b⟩ ∈ converse(r) <-> ⟨b, a⟩ ∈ r

lemma converseI:

      ⟨a, b⟩ ∈ r ==> ⟨b, a⟩ ∈ converse(r)

lemma converseD:

      ⟨a, b⟩ ∈ converse(r) ==> ⟨b, a⟩ ∈ r

lemma converseE:

      [| yx ∈ converse(r); !!x y. [| yx = ⟨y, x⟩; ⟨x, y⟩ ∈ r |] ==> P |] ==> P

lemma converse_converse:

      r ⊆ Sigma(A, B) ==> converse(converse(r)) = r

lemma converse_type:

      r ⊆ A × B ==> converse(r) ⊆ B × A

lemma converse_prod:

      converse(A × B) = B × A

lemma converse_empty:

      converse(0) = 0

lemma converse_subset_iff:

      A ⊆ Sigma(X, Y) ==> converse(A) ⊆ converse(B) <-> A ⊆ B

### Finite Set Constructions Using @{term cons}

lemma cons_subsetI:

      [| a ∈ C; B ⊆ C |] ==> cons(a, B) ⊆ C

lemma subset_consI:

      B ⊆ cons(a, B)

lemma cons_subset_iff:

      cons(a, B) ⊆ C <-> a ∈ C ∧ B ⊆ C

lemmas cons_subsetE:

      [| cons(a, B) ⊆ C; [| a ∈ C; B ⊆ C |] ==> R |] ==> R

lemmas cons_subsetE:

      [| cons(a, B) ⊆ C; [| a ∈ C; B ⊆ C |] ==> R |] ==> R

lemma subset_empty_iff:

      A ⊆ 0 <-> A = 0

lemma subset_cons_iff:

      C ⊆ cons(a, B) <-> C ⊆ B ∨ a ∈ C ∧ C - {a} ⊆ B

lemma cons_eq:

      {a} ∪ B = cons(a, B)

lemma cons_commute:

      cons(a, cons(b, C)) = cons(b, cons(a, C))

lemma cons_absorb:

      a ∈ B ==> cons(a, B) = B

lemma cons_Diff:

      a ∈ B ==> cons(a, B - {a}) = B

lemma Diff_cons_eq:

      cons(a, B) - C = (if a ∈ C then B - C else cons(a, B - C))

lemma equal_singleton:

      [| a ∈ C; !!y. y ∈ C ==> y = b |] ==> C = {b}

lemma

      cons(a, cons(a, B)) = cons(a, B)

lemma singleton_subsetI:

      a ∈ C ==> {a} ⊆ C

lemma singleton_subsetD:

      {a} ⊆ C ==> a ∈ C

lemma subset_succI:

      i ⊆ succ(i)

lemma succ_subsetI:

      [| i ∈ j; i ⊆ j |] ==> succ(i) ⊆ j

lemma succ_subsetE:

      [| succ(i) ⊆ j; [| i ∈ j; i ⊆ j |] ==> P |] ==> P

lemma succ_subset_iff:

      succ(a) ⊆ B <-> a ⊆ B ∧ a ∈ B

### Binary Intersection

lemma Int_subset_iff:

      C ⊆ A ∩ B <-> C ⊆ A ∧ C ⊆ B

lemma Int_lower1:

      A ∩ B ⊆ A

lemma Int_lower2:

      A ∩ B ⊆ B

lemma Int_greatest:

      [| C ⊆ A; C ⊆ B |] ==> C ⊆ A ∩ B

lemma Int_cons:

      cons(a, B) ∩ C ⊆ cons(a, B ∩ C)

lemma Int_absorb:

      A ∩ A = A

lemma Int_left_absorb:

      A ∩ (A ∩ B) = A ∩ B

lemma Int_commute:

      A ∩ B = B ∩ A

lemma Int_left_commute:

      A ∩ (B ∩ C) = B ∩ (A ∩ C)

lemma Int_assoc:

      A ∩ B ∩ C = A ∩ (B ∩ C)

lemmas Int_ac:

      A ∩ B ∩ C = A ∩ (B ∩ C)

      A ∩ (A ∩ B) = A ∩ B

      A ∩ B = B ∩ A

      A ∩ (B ∩ C) = B ∩ (A ∩ C)

lemmas Int_ac:

      A ∩ B ∩ C = A ∩ (B ∩ C)

      A ∩ (A ∩ B) = A ∩ B

      A ∩ B = B ∩ A

      A ∩ (B ∩ C) = B ∩ (A ∩ C)

lemma Int_absorb1:

      B ⊆ A ==> A ∩ B = B

lemma Int_absorb2:

      A ⊆ B ==> A ∩ B = A

lemma Int_Un_distrib:

      A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C

lemma Int_Un_distrib2:

      (B ∪ C) ∩ A = B ∩ A ∪ C ∩ A

lemma subset_Int_iff:

      A ⊆ B <-> A ∩ B = A

lemma subset_Int_iff2:

      A ⊆ B <-> B ∩ A = A

lemma Int_Diff_eq:

      C ⊆ A ==> (A - B) ∩ C = C - B

lemma Int_cons_left:

      cons(a, A) ∩ B = (if a ∈ B then cons(a, A ∩ B) else A ∩ B)

lemma Int_cons_right:

      A ∩ cons(a, B) = (if a ∈ A then cons(a, A ∩ B) else A ∩ B)

lemma cons_Int_distrib:

      cons(x, A ∩ B) = cons(x, A) ∩ cons(x, B)

### Binary Union

lemma Un_subset_iff:

      A ∪ B ⊆ C <-> A ⊆ C ∧ B ⊆ C

lemma Un_upper1:

      A ⊆ A ∪ B

lemma Un_upper2:

      B ⊆ A ∪ B

lemma Un_least:

      [| A ⊆ C; B ⊆ C |] ==> A ∪ B ⊆ C

lemma Un_cons:

      cons(a, B) ∪ C = cons(a, B ∪ C)

lemma Un_absorb:

      A ∪ A = A

lemma Un_left_absorb:

      A ∪ (A ∪ B) = A ∪ B

lemma Un_commute:

      A ∪ B = B ∪ A

lemma Un_left_commute:

      A ∪ (B ∪ C) = B ∪ (A ∪ C)

lemma Un_assoc:

      A ∪ B ∪ C = A ∪ (B ∪ C)

lemmas Un_ac:

      A ∪ B ∪ C = A ∪ (B ∪ C)

      A ∪ (A ∪ B) = A ∪ B

      A ∪ B = B ∪ A

      A ∪ (B ∪ C) = B ∪ (A ∪ C)

lemmas Un_ac:

      A ∪ B ∪ C = A ∪ (B ∪ C)

      A ∪ (A ∪ B) = A ∪ B

      A ∪ B = B ∪ A

      A ∪ (B ∪ C) = B ∪ (A ∪ C)

lemma Un_absorb1:

      A ⊆ B ==> A ∪ B = B

lemma Un_absorb2:

      B ⊆ A ==> A ∪ B = A

lemma Un_Int_distrib:

      A ∩ B ∪ C = (A ∪ C) ∩ (B ∪ C)

lemma subset_Un_iff:

      A ⊆ B <-> A ∪ B = B

lemma subset_Un_iff2:

      A ⊆ B <-> B ∪ A = B

lemma Un_empty:

      A ∪ B = 0 <-> A = 0 ∧ B = 0

lemma Un_eq_Union:

      A ∪ B = \<Union>{A, B}

### Set Difference

lemma Diff_subset:

      A - B ⊆ A

lemma Diff_contains:

      [| C ⊆ A; C ∩ B = 0 |] ==> C ⊆ A - B

lemma subset_Diff_cons_iff:

      B ⊆ A - cons(c, C) <-> B ⊆ A - C ∧ c ∉ B

lemma Diff_cancel:

      A - A = 0

lemma Diff_triv:

      A ∩ B = 0 ==> A - B = A

lemma empty_Diff:

      0 - A = 0

lemma Diff_0:

      A - 0 = A

lemma Diff_eq_0_iff:

      A - B = 0 <-> A ⊆ B

lemma Diff_cons:

      A - cons(a, B) = A - B - {a}

lemma Diff_cons2:

      A - cons(a, B) = A - {a} - B

lemma Diff_disjoint:

      A ∩ (B - A) = 0

lemma Diff_partition:

      A ⊆ B ==> A ∪ (B - A) = B

lemma subset_Un_Diff:

      A ⊆ B ∪ (A - B)

lemma double_complement:

      [| A ⊆ B; B ⊆ C |] ==> B - (C - A) = A

lemma double_complement_Un:

      A ∪ B - (B - A) = A

lemma Un_Int_crazy:

      A ∩ B ∪ B ∩ C ∪ C ∩ A = (A ∪ B) ∩ (B ∪ C) ∩ (C ∪ A)

lemma Diff_Un:

      A - (B ∪ C) = (A - B) ∩ (A - C)

lemma Diff_Int:

      A - B ∩ C = A - B ∪ (A - C)

lemma Un_Diff:

      A ∪ B - C = A - C ∪ (B - C)

lemma Int_Diff:

      A ∩ B - C = A ∩ (B - C)

lemma Diff_Int_distrib:

      C ∩ (A - B) = C ∩ A - C ∩ B

lemma Diff_Int_distrib2:

      (A - B) ∩ C = A ∩ C - B ∩ C

lemma Un_Int_assoc_iff:

      A ∩ B ∪ C = A ∩ (B ∪ C) <-> C ⊆ A

### Big Union and Intersection

lemma Union_subset_iff:

      \<Union>A ⊆ C <-> (∀x∈A. x ⊆ C)

lemma Union_upper:

      B ∈ A ==> B ⊆ \<Union>A

lemma Union_least:

      (!!x. x ∈ A ==> x ⊆ C) ==> \<Union>A ⊆ C

lemma Union_cons:

      \<Union>cons(a, B) = a ∪ \<Union>B

lemma Union_Un_distrib:

      \<Union>(A ∪ B) = \<Union>A ∪ \<Union>B

lemma Union_Int_subset:

      \<Union>(A ∩ B) ⊆ \<Union>A ∩ \<Union>B

lemma Union_disjoint:

      \<Union>C ∩ A = 0 <-> (∀B∈C. B ∩ A = 0)

lemma Union_empty_iff:

      \<Union>A = 0 <-> (∀B∈A. B = 0)

lemma Int_Union2:

      \<Union>B ∩ A = (\<Union>C∈B. C ∩ A)

lemma Inter_subset_iff:

      A ≠ 0 ==> C ⊆ \<Inter>A <-> (∀x∈A. C ⊆ x)

lemma Inter_lower:

      B ∈ A ==> \<Inter>A ⊆ B

lemma Inter_greatest:

      [| A ≠ 0; !!x. x ∈ A ==> C ⊆ x |] ==> C ⊆ \<Inter>A

lemma INT_lower:

      x ∈ A ==> (\<Inter>x∈A. B(x)) ⊆ B(x)

lemma INT_greatest:

      [| A ≠ 0; !!x. x ∈ A ==> C ⊆ B(x) |] ==> C ⊆ (\<Inter>x∈A. B(x))

lemma Inter_0:

      \<Inter>0 = 0

lemma Inter_Un_subset:

      [| z ∈ A; z ∈ B |] ==> \<Inter>A ∪ \<Inter>B ⊆ \<Inter>(A ∩ B)

lemma Inter_Un_distrib:

      [| A ≠ 0; B ≠ 0 |] ==> \<Inter>(A ∪ B) = \<Inter>A ∩ \<Inter>B

lemma Union_singleton:

      \<Union>{b} = b

lemma Inter_singleton:

      \<Inter>{b} = b

lemma Inter_cons:

      \<Inter>cons(a, B) = (if B = 0 then a else a ∩ \<Inter>B)

### Unions and Intersections of Families

lemma subset_UN_iff_eq:

      A ⊆ (\<Union>i∈I. B(i)) <-> A = (\<Union>i∈I. A ∩ B(i))

lemma UN_subset_iff:

      (\<Union>x∈A. B(x)) ⊆ C <-> (∀x∈A. B(x) ⊆ C)

lemma UN_upper:

      x ∈ A ==> B(x) ⊆ (\<Union>x∈A. B(x))

lemma UN_least:

      (!!x. x ∈ A ==> B(x) ⊆ C) ==> (\<Union>x∈A. B(x)) ⊆ C

lemma Union_eq_UN:

      \<Union>A = (\<Union>x∈A. x)

lemma Inter_eq_INT:

      \<Inter>A = (\<Inter>x∈A. x)

lemma UN_0:

      (\<Union>i∈0. A(i)) = 0

lemma UN_singleton:

      (\<Union>x∈A. {x}) = A

lemma UN_Un:

      (\<Union>i∈A ∪ B. C(i)) = (\<Union>i∈A. C(i)) ∪ (\<Union>i∈B. C(i))

lemma INT_Un:

      (\<Inter>i∈I ∪ J. A(i)) =
      (if I = 0 then \<Inter>j∈J. A(j)
       else if J = 0 then \<Inter>i∈I. A(i)
            else (\<Inter>i∈I. A(i)) ∩ (\<Inter>j∈J. A(j)))

lemma UN_UN_flatten:

      (\<Union>x∈\<Union>y∈A. B(y). C(x)) = (\<Union>y∈A. \<Union>x∈B(y). C(x))

lemma Int_UN_distrib:

      B ∩ (\<Union>i∈I. A(i)) = (\<Union>i∈I. B ∩ A(i))

lemma Un_INT_distrib:

      I ≠ 0 ==> B ∪ (\<Inter>i∈I. A(i)) = (\<Inter>i∈I. B ∪ A(i))

lemma Int_UN_distrib2:

      (\<Union>i∈I. A(i)) ∩ (\<Union>j∈J. B(j)) =
      (\<Union>i∈I. \<Union>j∈J. A(i) ∩ B(j))

lemma Un_INT_distrib2:

      [| I ≠ 0; J ≠ 0 |]
      ==> (\<Inter>i∈I. A(i)) ∪ (\<Inter>j∈J. B(j)) =
          (\<Inter>i∈I. \<Inter>j∈J. A(i) ∪ B(j))

lemma UN_constant:

      (\<Union>y∈A. c) = (if A = 0 then 0 else c)

lemma INT_constant:

      (\<Inter>y∈A. c) = (if A = 0 then 0 else c)

lemma UN_RepFun:

      (\<Union>y∈RepFun(A, f). B(y)) = (\<Union>x∈A. B(f(x)))

lemma INT_RepFun:

      (\<Inter>x∈RepFun(A, f). B(x)) = (\<Inter>a∈A. B(f(a)))

lemma INT_Union_eq:

      0 ∉ A ==> (\<Inter>x∈\<Union>A. B(x)) = (\<Inter>y∈A. \<Inter>x∈y. B(x))

lemma INT_UN_eq:

      ∀x∈A. B(x) ≠ 0
      ==> (\<Inter>z∈\<Union>x∈A. B(x). C(z)) = (\<Inter>x∈A. \<Inter>z∈B(x). C(z))

lemma UN_Un_distrib:

      (\<Union>i∈I. A(i) ∪ B(i)) = (\<Union>i∈I. A(i)) ∪ (\<Union>i∈I. B(i))

lemma INT_Int_distrib:

      I ≠ 0 ==> (\<Inter>i∈I. A(i) ∩ B(i)) = (\<Inter>i∈I. A(i)) ∩ (\<Inter>i∈I. B(i))

lemma UN_Int_subset:

      (\<Union>z∈I ∩ J. A(z)) ⊆ (\<Union>z∈I. A(z)) ∩ (\<Union>z∈J. A(z))

lemma Diff_UN:

      I ≠ 0 ==> B - (\<Union>i∈I. A(i)) = (\<Inter>i∈I. B - A(i))

lemma Diff_INT:

      I ≠ 0 ==> B - (\<Inter>i∈I. A(i)) = (\<Union>i∈I. B - A(i))

lemma Sigma_cons1:

      Sigma(cons(a, B), C) = {a} × C(a) ∪ Sigma(B, C)

lemma Sigma_cons2:

      A × cons(b, B) = A × {b} ∪ A × B

lemma Sigma_succ1:

      Sigma(succ(A), B) = {A} × B(A) ∪ Sigma(A, B)

lemma Sigma_succ2:

      A × succ(B) = A × {B} ∪ A × B

lemma SUM_UN_distrib1:

      (Σx∈\<Union>y∈A. C(y). B(x)) = (\<Union>y∈A. Σx∈C(y). B(x))

lemma SUM_UN_distrib2:

      (Σi∈I. \<Union>j∈J. C(i, j)) = (\<Union>j∈J. Σi∈I. C(i, j))

lemma SUM_Un_distrib1:

      (Σi∈I ∪ J. C(i)) = (Σi∈I. C(i)) ∪ (Σj∈J. C(j))

lemma SUM_Un_distrib2:

      (Σi∈I. A(i) ∪ B(i)) = (Σi∈I. A(i)) ∪ (Σi∈I. B(i))

lemma prod_Un_distrib2:

      I × (A ∪ B) = I × A ∪ I × B

lemma SUM_Int_distrib1:

      (Σi∈I ∩ J. C(i)) = (Σi∈I. C(i)) ∩ (Σj∈J. C(j))

lemma SUM_Int_distrib2:

      (Σi∈I. A(i) ∩ B(i)) = (Σi∈I. A(i)) ∩ (Σi∈I. B(i))

lemma prod_Int_distrib2:

      I × (A ∩ B) = I × A ∩ I × B

lemma SUM_eq_UN:

      (Σi∈I. A(i)) = (\<Union>i∈I. {i} × A(i))

lemma times_subset_iff:

      A' × B' ⊆ A × B <-> A' = 0 ∨ B' = 0 ∨ A' ⊆ A ∧ B' ⊆ B

lemma Int_Sigma_eq:

      (Σx∈A'. B'(x)) ∩ (Σx∈A. B(x)) = (Σx∈A' ∩ A. B'(x) ∩ B(x))

lemma domain_iff:

      a ∈ domain(r) <-> (∃y. ⟨a, y⟩ ∈ r)

lemma domainI:

      ⟨a, b⟩ ∈ r ==> a ∈ domain(r)

lemma domainE:

      [| a ∈ domain(r); !!y. ⟨a, y⟩ ∈ r ==> P |] ==> P

lemma domain_subset:

      domain(Sigma(A, B)) ⊆ A

lemma domain_of_prod:

      b ∈ B ==> domain(A × B) = A

lemma domain_0:

      domain(0) = 0

lemma domain_cons:

      domain(cons(⟨a, b⟩, r)) = cons(a, domain(r))

lemma domain_Un_eq:

      domain(A ∪ B) = domain(A) ∪ domain(B)

lemma domain_Int_subset:

      domain(A ∩ B) ⊆ domain(A) ∩ domain(B)

lemma domain_Diff_subset:

      domain(A) - domain(B) ⊆ domain(A - B)

lemma domain_UN:

      domain(\<Union>x∈A. B(x)) = (\<Union>x∈A. domain(B(x)))

lemma domain_Union:

      domain(\<Union>A) = (\<Union>x∈A. domain(x))

lemma rangeI:

      ⟨a, b⟩ ∈ r ==> b ∈ range(r)

lemma rangeE:

      [| b ∈ range(r); !!x. ⟨x, b⟩ ∈ r ==> P |] ==> P

lemma range_subset:

      range(A × B) ⊆ B

lemma range_of_prod:

      a ∈ A ==> range(A × B) = B

lemma range_0:

      range(0) = 0

lemma range_cons:

      range(cons(⟨a, b⟩, r)) = cons(b, range(r))

lemma range_Un_eq:

      range(A ∪ B) = range(A) ∪ range(B)

lemma range_Int_subset:

      range(A ∩ B) ⊆ range(A) ∩ range(B)

lemma range_Diff_subset:

      range(A) - range(B) ⊆ range(A - B)

lemma domain_converse:

      domain(converse(r)) = range(r)

lemma range_converse:

      range(converse(r)) = domain(r)

lemma fieldI1:

      ⟨a, b⟩ ∈ r ==> a ∈ field(r)

lemma fieldI2:

      ⟨a, b⟩ ∈ r ==> b ∈ field(r)

lemma fieldCI:

      (⟨c, a⟩ ∉ r ==> ⟨a, b⟩ ∈ r) ==> a ∈ field(r)

lemma fieldE:

      [| a ∈ field(r); !!x. ⟨a, x⟩ ∈ r ==> P; !!x. ⟨x, a⟩ ∈ r ==> P |] ==> P

lemma field_subset:

      field(A × B) ⊆ A ∪ B

lemma domain_subset_field:

      domain(r) ⊆ field(r)

lemma range_subset_field:

      range(r) ⊆ field(r)

lemma domain_times_range:

      r ⊆ Sigma(A, B) ==> r ⊆ domain(r) × range(r)

lemma field_times_field:

      r ⊆ Sigma(A, B) ==> r ⊆ field(r) × field(r)

lemma relation_field_times_field:

      relation(r) ==> r ⊆ field(r) × field(r)

lemma field_of_prod:

      field(A × A) = A

lemma field_0:

      field(0) = 0

lemma field_cons:

      field(cons(⟨a, b⟩, r)) = cons(a, cons(b, field(r)))

lemma field_Un_eq:

      field(A ∪ B) = field(A) ∪ field(B)

lemma field_Int_subset:

      field(A ∩ B) ⊆ field(A) ∩ field(B)

lemma field_Diff_subset:

      field(A) - field(B) ⊆ field(A - B)

lemma field_converse:

      field(converse(r)) = field(r)

lemma rel_Union:

      ∀x∈S. ∃A B. x ⊆ A × B ==> \<Union>S ⊆ domain(\<Union>S) × range(\<Union>S)

lemma rel_Un:

      [| r ⊆ A × B; s ⊆ C × D |] ==> r ∪ s ⊆ (A ∪ C) × (B ∪ D)

lemma domain_Diff_eq:

      [| ⟨a, c⟩ ∈ r; c ≠ b |] ==> domain(r - {⟨a, b⟩}) = domain(r)

lemma range_Diff_eq:

      [| ⟨c, b⟩ ∈ r; c ≠ a |] ==> range(r - {⟨a, b⟩}) = range(r)

### Image of a Set under a Function or Relation

lemma image_iff:

      b ∈ r `` A <-> (∃x∈A. ⟨x, b⟩ ∈ r)

lemma image_singleton_iff:

      b ∈ r `` {a} <-> ⟨a, b⟩ ∈ r

lemma imageI:

      [| ⟨a, b⟩ ∈ r; a ∈ A |] ==> b ∈ r `` A

lemma imageE:

      [| b ∈ r `` A; !!x. [| ⟨x, b⟩ ∈ r; x ∈ A |] ==> P |] ==> P

lemma image_subset:

      r ⊆ A × B ==> r `` C ⊆ B

lemma image_0:

      r `` 0 = 0

lemma image_Un:

      r `` (A ∪ B) = r `` A ∪ r `` B

lemma image_UN:

      r `` (\<Union>x∈A. B(x)) = (\<Union>x∈A. r `` B(x))

lemma Collect_image_eq:

      {z ∈ Sigma(A, B) . P(z)} `` C = (\<Union>x∈A. {y ∈ B(x) . x ∈ C ∧ P(⟨x, y⟩)})

lemma image_Int_subset:

      r `` (A ∩ B) ⊆ r `` A ∩ r `` B

lemma image_Int_square_subset:

      (r ∩ A × A) `` B ⊆ r `` B ∩ A

lemma image_Int_square:

      B ⊆ A ==> (r ∩ A × A) `` B = r `` B ∩ A

lemma image_0_left:

      0 `` A = 0

lemma image_Un_left:

      (r ∪ s) `` A = r `` A ∪ s `` A

lemma image_Int_subset_left:

      (r ∩ s) `` A ⊆ r `` A ∩ s `` A

### Inverse Image of a Set under a Function or Relation

lemma vimage_iff:

      a ∈ r -`` B <-> (∃y∈B. ⟨a, y⟩ ∈ r)

lemma vimage_singleton_iff:

      a ∈ r -`` {b} <-> ⟨a, b⟩ ∈ r

lemma vimageI:

      [| ⟨a, b⟩ ∈ r; b ∈ B |] ==> a ∈ r -`` B

lemma vimageE:

      [| a ∈ r -`` B; !!x. [| ⟨a, x⟩ ∈ r; x ∈ B |] ==> P |] ==> P

lemma vimage_subset:

      r ⊆ A × B ==> r -`` C ⊆ A

lemma vimage_0:

      r -`` 0 = 0

lemma vimage_Un:

      r -`` (A ∪ B) = r -`` A ∪ r -`` B

lemma vimage_Int_subset:

      r -`` (A ∩ B) ⊆ r -`` A ∩ r -`` B

lemma vimage_eq_UN:

      f -`` B = (\<Union>y∈B. f -`` {y})

lemma function_vimage_Int:

      function(f) ==> f -`` (A ∩ B) = f -`` A ∩ f -`` B

lemma function_vimage_Diff:

      function(f) ==> f -`` (A - B) = f -`` A - f -`` B

lemma function_image_vimage:

      function(f) ==> f `` (f -`` A) ⊆ A

lemma vimage_Int_square_subset:

      (r ∩ A × A) -`` B ⊆ r -`` B ∩ A

lemma vimage_Int_square:

      B ⊆ A ==> (r ∩ A × A) -`` B = r -`` B ∩ A

lemma vimage_0_left:

      0 -`` A = 0

lemma vimage_Un_left:

      (r ∪ s) -`` A = r -`` A ∪ s -`` A

lemma vimage_Int_subset_left:

      (r ∩ s) -`` A ⊆ r -`` A ∩ s -`` A

lemma converse_Un:

      converse(A ∪ B) = converse(A) ∪ converse(B)

lemma converse_Int:

      converse(A ∩ B) = converse(A) ∩ converse(B)

lemma converse_Diff:

      converse(A - B) = converse(A) - converse(B)

lemma converse_UN:

      converse(\<Union>x∈A. B(x)) = (\<Union>x∈A. converse(B(x)))

lemma converse_INT:

      converse(\<Inter>x∈A. B(x)) = (\<Inter>x∈A. converse(B(x)))

### Powerset Operator

lemma Pow_0:

      Pow(0) = {0}

lemma Pow_insert:

      Pow(cons(a, A)) = Pow(A) ∪ {cons(a, X) . X ∈ Pow(A)}

lemma Un_Pow_subset:

      Pow(A) ∪ Pow(B) ⊆ Pow(A ∪ B)

lemma UN_Pow_subset:

      (\<Union>x∈A. Pow(B(x))) ⊆ Pow(\<Union>x∈A. B(x))

lemma subset_Pow_Union:

      A ⊆ Pow(\<Union>A)

lemma Union_Pow_eq:

      \<Union>Pow(A) = A

lemma Union_Pow_iff:

      \<Union>A ∈ Pow(B) <-> A ∈ Pow(Pow(B))

lemma Pow_Int_eq:

      Pow(A ∩ B) = Pow(A) ∩ Pow(B)

lemma Pow_INT_eq:

      A ≠ 0 ==> Pow(\<Inter>x∈A. B(x)) = (\<Inter>x∈A. Pow(B(x)))

### RepFun

lemma RepFun_subset:

      (!!x. x ∈ A ==> f(x) ∈ B) ==> {f(x) . x ∈ A} ⊆ B

lemma RepFun_eq_0_iff:

      {f(x) . x ∈ A} = 0 <-> A = 0

lemma RepFun_constant:

      {c . x ∈ A} = (if A = 0 then 0 else {c})

### Collect

lemma Collect_subset:

      Collect(A, P) ⊆ A

lemma Collect_Un:

      Collect(A ∪ B, P) = Collect(A, P) ∪ Collect(B, P)

lemma Collect_Int:

      Collect(A ∩ B, P) = Collect(A, P) ∩ Collect(B, P)

lemma Collect_Diff:

      Collect(A - B, P) = Collect(A, P) - Collect(B, P)

lemma Collect_cons:

      {x ∈ cons(a, B) . P(x)} =
      (if P(a) then cons(a, {x ∈ B . P(x)}) else {x ∈ B . P(x)})

lemma Int_Collect_self_eq:

      A ∩ Collect(A, P) = Collect(A, P)

lemma Collect_Collect_eq:

      Collect(Collect(A, P), Q) = {x ∈ A . P(x) ∧ Q(x)}

lemma Collect_Int_Collect_eq:

      Collect(A, P) ∩ Collect(A, Q) = {x ∈ A . P(x) ∧ Q(x)}

lemma Collect_Union_eq:

      Collect(\<Union>x∈A. B(x), P) = (\<Union>x∈A. Collect(B(x), P))

lemma Collect_Int_left:

      {x ∈ A . P(x)} ∩ B = {x ∈ A ∩ B . P(x)}

lemma Collect_Int_right:

      A ∩ {x ∈ B . P(x)} = {x ∈ A ∩ B . P(x)}

lemma Collect_disj_eq:

      {x ∈ A . P(x) ∨ Q(x)} = Collect(A, P) ∪ Collect(A, Q)

lemma Collect_conj_eq:

      {x ∈ A . P(x) ∧ Q(x)} = Collect(A, P) ∩ Collect(A, Q)

lemmas subset_SIs:

      A ⊆ A

      [| a ∈ C; B ⊆ C |] ==> cons(a, B) ⊆ C

      B ⊆ cons(a, B)

      (!!x. x ∈ A ==> x ⊆ C) ==> \<Union>A ⊆ C

      (!!x. x ∈ A ==> B(x) ⊆ C) ==> (\<Union>x∈A. B(x)) ⊆ C

      [| A ⊆ C; B ⊆ C |] ==> A ∪ B ⊆ C

      [| A ≠ 0; !!x. x ∈ A ==> C ⊆ x |] ==> C ⊆ \<Inter>A

      [| C ⊆ A; C ⊆ B |] ==> C ⊆ A ∩ B

      (!!x. x ∈ A ==> f(x) ∈ B) ==> {f(x) . x ∈ A} ⊆ B

      A ⊆ A ∪ B

      B ⊆ A ∪ B

      A ∩ B ⊆ A

      A ∩ B ⊆ B

lemmas subset_SIs:

      A ⊆ A

      [| a ∈ C; B ⊆ C |] ==> cons(a, B) ⊆ C

      B ⊆ cons(a, B)

      (!!x. x ∈ A ==> x ⊆ C) ==> \<Union>A ⊆ C

      (!!x. x ∈ A ==> B(x) ⊆ C) ==> (\<Union>x∈A. B(x)) ⊆ C

      [| A ⊆ C; B ⊆ C |] ==> A ∪ B ⊆ C

      [| A ≠ 0; !!x. x ∈ A ==> C ⊆ x |] ==> C ⊆ \<Inter>A

      [| C ⊆ A; C ⊆ B |] ==> C ⊆ A ∩ B

      (!!x. x ∈ A ==> f(x) ∈ B) ==> {f(x) . x ∈ A} ⊆ B

      A ⊆ A ∪ B

      B ⊆ A ∪ B

      A ∩ B ⊆ A

      A ∩ B ⊆ B