(def-theorem empty_indic-is-empty"empty_indic_q{empty_indic{uu}}"(theory indicators) (usages transportable transportable-rewrite) (proof (simplify-insistently)))

(def-theorem equals-empty-indic-iff-empty"forall(a:sets[uu], a=empty_indic{uu} iff empty_indic_q{a})"reverse (theory indicators) (usages transportable transportable-rewrite) (proof ( direct-and-antecedent-inference-strategy (backchain"with(a:sets[uu],a=empty_indic{uu})") (apply-macete-with-minor-premises empty_indic-is-empty) extensionality beta-reduce-repeatedly )))

(def-theorem union-commutativity"forall(a,b:sets[uu], (a union b) = (b union a))"(theory indicators) (usages transportable-macete) (proof ( direct-inference extensionality direct-inference simplify-insistently (case-split-on-conditionals (0)) )))

(def-theorem intersection-commutativity"forall(a,b:sets[uu], (a inters b) = (b inters a))"(theory indicators) (usages transportable-macete) (proof ( direct-inference extensionality direct-inference simplify-insistently (case-split-on-conditionals (0)) simplify (contrapose"with(p:prop, p)") simplify )))

(def-theorem membership-in-union"forall(x:uu,a,b:sets[uu], x in (a union b) iff (x in a or x in b))"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem membership-in-intersection"forall(x:uu,a,b:sets[uu], x in (a inters b) iff (x in a and x in b))"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem diff-union-equal-whole"forall(x:uu,a,b:sets[uu], b subseteq a implies (a diff b) union b = a)"(theory indicators) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy extensionality direct-inference simplify (instantiate-universal-antecedent"with(p:prop,p);"("x_0")) (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 0)") direct-and-antecedent-inference-strategy simplify) (block (script-comment"node added by `instantiate-universal-antecedent' at (0 0 1)") direct-and-antecedent-inference-strategy simplify) )))

(def-theorem element-of-a-subset-is-an-element ;"forall(x:uu,b:sets[uu], forsome(a:sets[uu], (x in a) and (a subseteq b)) implies (x in b))"(theory indicators) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(b,a:sets[uu],a subseteq b)"("x")) )))

(def-theorem subseteq-reflexivity"forall(a:sets[uu], a subseteq a)"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem subseteq-antisymmetry"forall(a,b:sets[uu], a=b iff ((a subseteq b) and (b subseteq a)))"(theory indicators) (usages transportable-macete) (proof; 38 nodes ( insistent-direct-inference-strategy (force-substitution"b""a"(0)) (force-substitution"a""b"(0)) extensionality direct-inference (antecedent-inference"with(b,a:sets[uu],a subseteq b and b subseteq a)") (instantiate-universal-antecedent"with(a,b:sets[uu],b subseteq a)"("x_0")) (instantiate-universal-antecedent"with(b,a:sets[uu],a subseteq b)"("x_0")) simplify (instantiate-universal-antecedent"with(b,a:sets[uu],a subseteq b)"("x_0")) simplify )))

(def-theorem subseteq-transitivity"forall(a,b,c:sets[uu], (a subseteq b) and (b subseteq c) implies (a subseteq c))"(theory indicators) (usages transportable-macete) (proof ( insistent-direct-inference-strategy simplify-insistently )))

(def-theorem union-disjunction-conversion"forall(x:uu, a,b:sets[uu], (x in (a union b)) iff (x in a or x in b))"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem intersection-conjunction-conversion"forall(x:uu, a,b:sets[uu], (x in (a inters b)) iff (x in a and x in b))"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem singleton-equality-conversion"forall(x,a:uu,x in singleton{a} iff x=a)"(theory indicators) (usages transportable-rewrite transportable-macete) (proof (simplify-insistently)))

(def-theorem difference-conjunction-conversion"forall(x:uu, a,b:sets[uu], (x in (a diff b)) iff (x in a and not (x in b)))"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-compound-macete indicator-conversions (repeat tr%union-disjunction-conversion tr%intersection-conjunction-conversion tr%singleton-equality-conversion tr%difference-conjunction-conversion))

(def-theorem big-union-member"forall(f:[index,sets[uu]],x:uu, x in big_u{f} iff forsome(i:index,x in f(i)))"(theory family-indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem big-intersection-member"forall(f:[index,sets[uu]], x:uu, x in big_i{f} iff forall(i:index,x in f(i)))"(theory family-indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem in-singleton-iff-equals-single-member"forall(x,y:uu, x in singleton{y} iff x=y)"reverse (theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem singletons-have-a-unique-member"forall(a:sets[uu],y:uu, a=singleton{y} iff y=iota(x:uu, x in a))"(theory indicators) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (force-substitution"a""singleton{y}"(0)) beta-reduce-insistently (contrapose"with(y:uu,a:sets[uu],a=singleton{y})") extensionality (instantiate-existential ("b_$0")) simplify (force-substitution"y""iota(x:uu,x in a)"(0)) (eliminate-defined-iota-expression 0 u) extensionality direct-inference (instantiate-universal-antecedent"with(p:prop, forall(u_1:uu,p))"("x_0")) simplify (raise-conditional (0)) direct-and-antecedent-inference-strategy (simplify-antecedent"with(x_0:uu,a:sets[uu],not(x_0 in a))") simplify )))

(def-theorem diff-with-indic-is-disj-from-indic"forall(a,b:sets[uu], (a diff b) disj b)"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem membership-in-diff"forall(x:uu,a,b:sets[uu], (x in a diff b) iff (x in a and not(x in b)))"(theory indicators) (usages transportable-macete) (proof (simplify-insistently)))

(def-theorem decremented-partition-lemma"forall(w:sets[sets[uu]],a,b:sets[uu], partition_q{w,a} and b in w implies partition_q{w diff singleton{b},a diff b})"(theory indicators) (usages transportable-macete) (proof; 74 nodes ( direct-and-antecedent-inference-strategy insistent-direct-inference direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(u,v:sets[uu],p))"("u_$0""v_$0")) (contrapose"with(p:prop, not(p))") (weaken (0 1 3 4 5)) (incorporate-antecedent"with(p:prop, p)") simplify-insistently (contrapose"with(p:prop, not(p))") (weaken (0 2 3 4 5)) (incorporate-antecedent"with(p:prop, p)") simplify-insistently (weaken (0)) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(x:uu,p))"("x_$0")) (instantiate-existential ("u")) extensionality (instantiate-existential ("x_$0")) simplify (backchain"with(p:prop, forall(x:uu,p))") (instantiate-existential ("u_$0")) (instantiate-universal-antecedent"with(p:prop, forall(u,v:sets[uu],p))"("u_$0""b")) (weaken (2 3 4 5 6)) (incorporate-antecedent"with(p:prop, p)") simplify-insistently )))

(def-theorem union-of-a-difference"forall(a,b:sets[uu], a subseteq b implies a union (b diff a) = b)"(theory indicators) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises subseteq-antisymmetry) simplify-insistently direct-and-antecedent-inference-strategy (backchain"with(b,a:sets[uu],a subseteq b);") )))

(def-theorem difference-of-a-disjoint-union"forall(a,b:sets[uu], a inters b=empty_indic{uu} implies (a union b) diff a = b)"(theory indicators) (usages transportable-macete) (proof ( (prove-by-logic-and-simplification 0) (block (script-comment"node added by `prove-by-logic-and-simplification' at (0 0 0 (1 . 0) 0 0 0 0 (1 . 1) (1 . 0) 1 0)") (contrapose"with(f:sets[uu],f=f);") simplify-insistently extensionality (instantiate-existential ("x_0")) simplify) (contrapose"with(f:sets[uu],f=f);"))))

(def-theorem difference-of-disjoint-sets"forall(a,b:sets[uu], a inters b=empty_indic{uu} implies a diff b = a)"(theory indicators) (usages transportable-macete) (proof ( simplify-insistently (prove-by-logic-and-simplification 0) (contrapose"with(f:sets[uu],f=f);") (prove-by-logic-and-simplification 0) auto-instantiate-existential)))

(def-theorem difference-of-a-union"forall(a,b:sets[uu], (a union b) diff a = b diff a)"(theory indicators) (usages transportable-macete) (proof ( (prove-by-logic-and-simplification 0))))

(def-theorem union-with-empty"forall(a:sets[uu], (a union empty_indic{uu}) = a)"(theory indicators) (usages transportable-macete) (proof ((prove-by-logic-and-simplification 0))))