```
(def-theorem unary-eta-reduction
"forall(f:[ind_1,ind_2], lambda(x:ind_1,f(x))=f);"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-inference
extensionality
simplify
)))
```

```
(def-theorem domain-membership-iff-defined
"forall(x:ind_1,f:[ind_1,ind_2], x in dom(f) iff #(f(x)))"
reverse
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof (simplify-insistently)))
```

```
(def-theorem range-domain-membership
"forall(x:ind_1,f:[ind_1,ind_2], f(x) in ran{f} iff x in dom(f))"
reverse
(theory pure-generic-theory-2)
(usages transportable-macete transportable-rewrite)
(proof
(
simplify-insistently
direct-and-antecedent-inference-strategy
simplify-insistently
(instantiate-existential ("x"))
)))
```

```
(def-theorem membership-in-a-domain
"forall(x:ind_1,a:sets[ind_1],f:[ind_1,ind_2],
dom{f}=a and #(f(x)) implies x in a)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "a" "dom{f}" (0))
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
)))
```

```
(def-theorem membership-in-a-range
"forall(x:ind_1,y:ind_2,b:sets[ind_2],f:[ind_1,ind_2],
ran{f}=b and y=f(x) implies y in b)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "b" "ran{f}" (0))
(force-substitution "y" "f(x)" (0))
(apply-macete-with-minor-premises tr%range-domain-membership)
simplify-insistently
)))
```

```
(def-theorem dom-of-an-indicator
"forall(a:sets[ind_1], dom{a}=a)"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-inference
extensionality
extensionality
direct-inference
simplify-insistently
(case-split-on-conditionals (0))
)))
```

```
(def-theorem associativity-of-composition
"forall(f:[ind_3,ind_4],g:[ind_2,ind_3],h:[ind_1,ind_2],
(f oo g) oo h = f oo (g oo h))"
reverse
(theory pure-generic-theory-4)
(usages transportable-macete)
(proof
(
direct-inference
extensionality
direct-inference
simplify
)))
```

```
(def-theorem composition-decreases-domain
"forall(f:[ind_1,ind_2], g:[ind_2,ind_3],
dom{g oo f} subseteq dom{f})"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof (simplify-insistently)))
```

```
(def-theorem composition-decreases-range
"forall(f:[ind_1,ind_2], g:[ind_2,ind_3],
ran{g oo f} subseteq ran{g})"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof
(
simplify-insistently
direct-and-antecedent-inference-strategy
auto-instantiate-existential
)))
```

```
(def-theorem domain-composition
"forall(f:[ind_1,ind_2], g:[ind_2,ind_3],
ran{f} subseteq dom{g} implies dom{g oo f} = dom{f})"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof
(
simplify-insistently
direct-and-antecedent-inference-strategy
extensionality
direct-and-antecedent-inference-strategy
simplify
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(p));")
(instantiate-universal-antecedent "with(p:prop,forall(x_\$0:ind_2,p));"
("f(x_0)"))
(instantiate-universal-antecedent "with(p:prop,forall(x_\$1:ind_1,p));" ("x_0")))))
```

```
(def-theorem range-composition
"forall(f:[ind_1,ind_2], g:[ind_2,ind_3],
dom{g} subseteq ran{f} implies ran{g oo f} = ran{g})"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof
(

simplify-insistently
direct-and-antecedent-inference-strategy
extensionality
direct-and-antecedent-inference-strategy
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0)")
(contrapose "with(p:prop,not(p));")
(instantiate-universal-antecedent "with(p:prop,forall(x_\$0:ind_2,p));"
("x"))
(instantiate-existential ("x_\$1"))
simplify))))
```

```
(def-theorem injective-composition
"forall(f:[ind_1,ind_2], g:[ind_2,ind_3],
injective_q{f} and injective_on_q{g,ran{f}} implies injective_q{g oo f})"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
direct-inference
(backchain "with(f:[ind_1,ind_2],injective_q{f})")
(backchain
"with(g:[ind_2,ind_3],f:[ind_1,ind_2], injective_on_q{g,ran{f}})")
(incorporate-antecedent "with(x,y:ind_3, x=y)")
(weaken (0 1))
simplify-insistently
direct-and-antecedent-inference-strategy
(instantiate-existential ("x_\$0"))
(instantiate-existential ("x_\$1"))
simplify
)))
```

```
(def-theorem image-of-domain-is-range
"forall(f:[ind_1,ind_2], image{f,dom{f}} = ran{f})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-inference
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
insistent-direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(instantiate-existential ("x_\$1"))
insistent-direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
(instantiate-existential ("x"))
)))
```

```
(def-theorem image-subset-of-range-characterization
"forall(s:sets[ind_1],f:[ind_1,ind_2],
s subseteq dom{f} implies image{f,s} subseteq ran{f})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
auto-instantiate-existential
)))
```

```
(def-theorem image-is-monotone-wrt-subseteq
"forall(f:[ind_1,ind_2],a,b:sets[ind_1],
(a subseteq b) implies (image(f,a) subseteq image(f,b)))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
simplify-insistently
direct-and-antecedent-inference-strategy
auto-instantiate-existential
(backchain "with(b,a:sets[ind_1],a subseteq b)")
)))
```

```
(def-theorem direct-image-disjointness-conversion
"forall(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
empty_indic_q(b inters image(f,a)) iff empty_indic_q(inv_image(f,b) inters a))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(p:prop, forall(x_\$0:ind_2,p))")
auto-instantiate-existential
(contrapose "with(p:prop, forall(x_\$0:ind_1,p))")
auto-instantiate-existential
simplify
)))
```

```
(def-theorem direct-image-subset-conversion
"forall(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
total_q(f,[ind_1,ind_2])
implies
(image(f,a) subseteq b iff a subseteq inv_image(f,b)))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(p:prop, forall(x_\$0:ind_2,p))")
auto-instantiate-existential
(auto-instantiate-universal-antecedent "with(p:prop, forall(x_\$0:ind_1,p))")
simplify
)))
```

```
(def-theorem inverse-image-union-preservation
"forall(f:[ind_1,ind_2],a,b:sets[ind_2],
inv_image(f,a union b) = inv_image(f,a) union inv_image(f,b))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
simplify-insistently
direct-and-antecedent-inference-strategy
(contrapose "with(y:ind_2,a:sets[ind_2], y in a)")
(case-split ("#(f(x_\$2))"))
(apply-macete-with-minor-premises tr%membership-in-union)
simplify
simplify
(apply-macete-with-minor-premises tr%membership-in-union)
simplify
(apply-macete-with-minor-premises tr%membership-in-union)
simplify
)))
```

```
(def-theorem inverse-image-inters-preservation
"forall(f:[ind_1,ind_2],a,b:sets[ind_2],
inv_image(f,a inters b) = inv_image(f,a) inters inv_image(f,b))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
simplify-insistently
(apply-macete-with-minor-premises tr%membership-in-intersection)
)))
```

```
(def-theorem meaning-of-inverse-image-membership
"forall(f:[ind_1,ind_2],x:ind_1,o:sets[ind_2],
x in inv_image(f,o) iff f(x) in o)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof (simplify-insistently)))
```

```
(def-compound-macete direct-image-to-inverse-image-conversion-macete
(repeat
tr%direct-image-disjointness-conversion
tr%direct-image-subset-conversion
tr%inverse-image-union-preservation
tr%inverse-image-inters-preservation))
```

```
(def-compound-macete indicator-facts-macete
(repeat
tr%meaning-of-indic-from-pred-element
tr%meaning-of-inverse-image-membership))
```

```
(def-theorem dom-of-id
"forall(a:sets[ind_1], dom{id{a}} = a)"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-inference
extensionality
direct-inference
simplify-insistently
(case-split-on-conditionals (0))
)))
```

```
(def-theorem ran-of-id
"forall(a:sets[ind_1], ran{id{a}} = a)"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
direct-inference
extensionality
direct-inference
simplify-insistently
(case-split-on-conditionals (0))
(antecedent-inference "with(p:prop, forsome(x_\$1:ind_1,p))")
(incorporate-antecedent "with(x,y:ind_1, x=y)")
(case-split-on-conditionals (0))
(contrapose "with(p:prop, not(p))")
(instantiate-existential ("x_0"))
simplify
)))
```

```
(def-theorem id-is-injective-on-dom
"forall(a:sets[ind_1], injective_on_q{id{a},a})"
(theory pure-generic-theory-1)
(usages transportable-macete)
(proof
(
insistent-direct-inference-strategy
(antecedent-inference "with(p,q,r:prop, p and q and r)")
(incorporate-antecedent "with(x,y:ind_1, x = y)")
simplify-insistently
)))
```

```
(def-theorem composition-with-id-right
"forall(f:[ind_1,ind_2], a:sets[ind_1], f oo id{a} = restrict{f,a})"
(theory pure-generic-theory-2)
(usages transportable-macete transportable-rewrite)
(proof
(
direct-inference
extensionality
direct-inference
simplify
(case-split-on-conditionals (0)))))
```

```
(def-theorem composition-with-id-left
"forall(f:[ind_1,ind_2],a:sets[ind_2],
id{a} oo f = restrict{f,inv_image{f,a}})"
(theory pure-generic-theory-2)
(usages transportable-macete transportable-rewrite)
(proof
(
direct-inference
extensionality
direct-inference
simplify
(case-split-on-conditionals (0))
)))
```

```
(def-theorem composition-with-total-id-left
"forall(f:[ind_1,ind_2],a:sets[ind_2],
total_q{a,sets[ind_2]} implies id{a} oo f = f)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
extensionality
direct-inference
(case-split ("#(f(x_0))"))
simplify
simplify
)))
```

```
(def-theorem composition-with-total-id-right
"forall(f:[ind_1,ind_2], a:sets[ind_1],
total_q{a,sets[ind_1]} implies f oo id{a} = f)"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
extensionality
direct-inference
(case-split ("#(f(x_0))"))
simplify
simplify
)))
```

```
(def-theorem surjective-on-lemma
"forall(a:sets[ind_1],b:sets[ind_2],f:[ind_1,ind_2],x:ind_1,
surjective_on_q(f,a,b) and (x in a) implies (f(x) in b))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "b" "ran{f}" (0))
(apply-macete-with-minor-premises tr%range-domain-membership)
simplify
)))
```

```
(def-theorem domain-of-a-bijective-composition
"forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],f:[ind_1,ind_2],g:[ind_2,ind_3],
bijective_on_q(f,a,b) and bijective_on_q(g,b,c) implies dom(g oo f) = a)"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%domain-composition)
)))
```

```
(def-theorem range-of-a-bijective-composition
"forall(a:sets[ind_1],b:sets[ind_2],c:sets[ind_3],f:[ind_1,ind_2],g:[ind_2,ind_3],
bijective_on_q(f,a,b) and bijective_on_q(g,b,c) implies ran(g oo f) = c)"
(theory pure-generic-theory-3)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%range-composition)
)))
```

```
(def-theorem injective-and-surjective-is-total
"forall(f:[ind_1,ind_2],
injective_q{f} and surjective_q{f} implies total_q{f,[ind_1,ind_2]})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof (simplify-insistently)))
```

```
(def-theorem injective-implies-injective-on
"forall(f:[ind_1,ind_2],a:sets[ind_1],
injective_q{f} implies injective_on_q{f,a})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
insistent-direct-inference-strategy
simplify
)))
```

```
(def-theorem injective-iff-injective-on-domain
"forall(f:[ind_1,ind_2],a:sets[ind_1],
injective_q{f} iff injective_on_q{f,dom{f}})"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises injective-implies-injective-on)
insistent-direct-inference
direct-inference
(backchain "with(f:[ind_1,ind_2],injective_on_q{f,dom{f}});")
simplify
)))
```

```
(def-theorem range-of-bijection-on-singleton
"forall(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
bijective_on_q{f,a,b} and forsome(x:ind_1,a=singleton{x})
implies
forsome(y:ind_2,b=singleton{y}))"
(theory pure-generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forall(y:ind_1, y in a iff y=x)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "#(f(x))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-with-minor-premises tr%singletons-have-a-unique-member)
(instantiate-existential ("f(x)"))
(backchain-backwards "with(b:sets[ind_2],f:[ind_1,ind_2],ran{f}=b);")
beta-reduce-insistently
simplify
(apply-macete-with-minor-premises eliminate-iota-macete)
direct-inference
(instantiate-existential ("x"))
(block
(script-comment "`direct-inference' at (1)")
direct-and-antecedent-inference-strategy
(backchain "with(i,b_\$0:ind_2,b_\$0=i);")
(instantiate-universal-antecedent "with(p:prop,forall(y:ind_1,p));"
("x_\$1"))
(contrapose "with(x_\$1:ind_1,a:sets[ind_1],not(x_\$1 in a));")
(backchain-backwards "with(a:sets[ind_1],f:[ind_1,ind_2],dom{f}=a);")
(apply-macete-with-minor-premises domain-membership-iff-defined)))
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises rev%domain-membership-iff-defined)
(force-substitution "dom{f}" "singleton{x}" (0))
(weaken (0 1 2 3 4))
simplify-insistently))
(block
(script-comment "`cut-with-single-formula' at (1)")
(backchain "with(x:ind_1,a:sets[ind_1],a=singleton{x});")
(weaken (0 1 2 3))
simplify-insistently)
)))
```

```
(def-theorem restricted-to-range-composition-lemma
"forall(phi:[ind_1,ind_2],f:[ind_2,ind_3],
f oo phi==(restrict{f,ran{phi}}) oo phi)"
(theory generic-theory-3)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
simplify-insistently
extensionality
direct-and-antecedent-inference-strategy
(case-split ("#(phi(x_0))"))
simplify
(cut-with-single-formula "forsome(x_\$1:ind_1,phi(x_0)=phi(x_\$1))")
simplify
(instantiate-existential ("x_0"))
simplify
)))
```

```
(def-theorem domain-of-a-restriction
"forall(phi:[ind_1,ind_2], s:sets[ind_1], s subseteq dom{phi} implies
s=dom{restrict{phi,s}})"
(theory generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
insistent-direct-inference
direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
simplify
(apply-macete-with-minor-premises rev%domain-membership-iff-defined)
(backchain "with(phi:[ind_1,ind_2],s:sets[ind_1],s subseteq dom{phi});")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
)))
```

```
(def-theorem image-of-a-restriction
"forall(phi:[ind_1,ind_2], s:sets[ind_1],image{restrict{phi,s},s}=image{phi,s})"
(theory generic-theory-2)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-existential ("x_\$1"))
(contrapose "with(phi:[ind_1,ind_2],x_\$1:ind_1,s:sets[ind_1],x_\$2:ind_2,
x_\$2=if(x_\$1 in s, phi(x_\$1), ?ind_2));")
simplify
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
auto-instantiate-existential
simplify
)))
```

```
(def-theorem injectivity-of-a-restriction
"forall(phi:[ind_1,ind_2], s:sets[ind_1],injective_q{phi}
implies injective_q{restrict{phi,s}})"
(theory generic-theory-2)
(usages transportable-macete)
(proof
(

insistent-direct-inference-strategy
(backchain "with(phi:[ind_1,ind_2],injective_q{phi});")
(case-split ("x_1 in s " "x_2 in s"))
(contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
simplify
(contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
simplify
(contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
simplify
(contrapose "with(x_2,x_1:ind_1,phi:[ind_1,ind_2],s:sets[ind_1],
restrict{phi,s}(x_1)=restrict{phi,s}(x_2));")
simplify
)))
```