```
(def-theorem sb-symmetry-obl
"forall(h_0:[nn,sets[ind_2]],h_1:[nn,sets[ind_1]],
forall(u_0:nn,
#(if(u_0=0,
dom{g},
lambda(dummy_\$0:sets[ind_1],
if(#(dummy_\$0), image{f,dummy_\$0}, ?sets[ind_2]))(h_1(u_0-1))))
implies
if(u_0=0,
dom{g},
lambda(dummy_\$0:sets[ind_1],
if(#(dummy_\$0), image{f,dummy_\$0}, ?sets[ind_2]))(h_1(u_0-1)))=h_0(u_0))
and
forall(u_0:nn,
#(if(u_0=0,
dom{f},
lambda(dummy_\$1:sets[ind_2],
if(#(dummy_\$1), image{g,dummy_\$1}, ?sets[ind_1]))(h_0(u_0-1))))
implies
if(u_0=0,
dom{f},
lambda(dummy_\$1:sets[ind_2],
if(#(dummy_\$1), image{g,dummy_\$1}, ?sets[ind_1]))(h_0(u_0-1)))=h_1(u_0))
implies
forall(u_0:nn,#(b%seq(u_0)) implies b%seq(u_0)=h_0(u_0))
and
forall(u_0:nn,#(a%seq(u_0)) implies a%seq(u_0)=h_1(u_0)))"
lemma
(theory schroeder-bernstein-theory)
(proof
(
(assume-theorem
schroeder-bernstein-set-functions-strong-minimality_schroeder-bernstein-theory)
direct-and-antecedent-inference-strategy
(backchain "with(p:prop, forall(h_0:[nn,sets[ind_1]],h_1:[nn,sets[ind_2]], p))")
direct-inference
auto-instantiate-existential
(backchain "with(p:prop, forall(h_0:[nn,sets[ind_1]],h_1:[nn,sets[ind_2]], p))")
direct-inference
auto-instantiate-existential
)))
```

```
(def-theorem sb->gt2-obl-1
"forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1],
nonempty_indic_q{a}
and
nonempty_indic_q{b}
and
dom{u}=a
and
dom{v}=b
and
ran{u} subseteq b
and
ran{v} subseteq a
and
injective_on_q{u,a}
and
injective_on_q{v,b}
implies
forall(x_\$0:ind_1,
if_form(x_\$0 in a,
#(u(x_\$0)) implies u(x_\$0) in b,
not(#(u(x_\$0))))))"
lemma
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%element-of-a-subset-is-an-element)
auto-instantiate-existential
(apply-macete-with-minor-premises range-domain-membership)
(apply-macete-with-minor-premises domain-membership-iff-defined)
(apply-macete-with-minor-premises rev%domain-membership-iff-defined)
(backchain "with(a:sets[ind_1],u:[ind_1,ind_2],dom{u}=a)")
)))
```

```
(def-theorem sb->gt2-obl-2
"forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1],
nonempty_indic_q{a}
and
nonempty_indic_q{b}
and
dom{u}=a
and
dom{v}=b
and
ran{u} subseteq b
and
ran{v} subseteq a
and
injective_on_q{u,a}
and
injective_on_q{v,b}
implies
forall(x_\$0:ind_2,
if_form(x_\$0 in b,
#(v(x_\$0)) implies v(x_\$0) in a,
not(#(v(x_\$0))))))"
lemma
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%element-of-a-subset-is-an-element)
auto-instantiate-existential
(apply-macete-with-minor-premises tr%range-domain-membership)
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(backchain "with(b:sets[ind_2],v:[ind_2,ind_1],dom{v}=b)")
)))
```

```
(def-theorem sb->gt2-obl-3
"forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1],
nonempty_indic_q{a}
and
nonempty_indic_q{b}
and
dom{u}=a
and
dom{v}=b
and
ran{u} subseteq b
and
ran{v} subseteq a
and
injective_on_q{u,a}
and
injective_on_q{v,b}
implies
forall(x_0:ind_1,x_0 in a implies #(u(x_0))))"
lemma
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises rev%domain-membership-iff-defined)
(backchain "with(a:sets[ind_1],u:[ind_1,ind_2],dom{u}=a)")
)))
```

```
(def-theorem sb->gt2-obl-4
"forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1],
nonempty_indic_q{a}
and
nonempty_indic_q{b}
and
dom{u}=a
and
dom{v}=b
and
ran{u} subseteq b
and
ran{v} subseteq a
and
injective_on_q{u,a}
and
injective_on_q{v,b}
implies
forall(x_0:ind_2,x_0 in b implies #(v(x_0))))"
lemma
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(backchain "with(b:sets[ind_2],v:[ind_2,ind_1],dom{v}=b)")
)))
```

```
(def-theorem sb->gt2-obl-5
"forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1],
nonempty_indic_q{a}
and
nonempty_indic_q{b}
and
dom{u}=a
and
dom{v}=b
and
ran{u} subseteq b
and
ran{v} subseteq a
and
injective_on_q{u,a}
and
injective_on_q{v,b}
implies
forall(x_1,x_2:ind_1,
x_1 in a and x_2 in a
implies
(u(x_1)=u(x_2) implies x_1=x_2)))"
lemma
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(backchain "with(u:[ind_1,ind_2],a:sets[ind_1],injective_on_q{u,a})")
direct-inference
)))
```

```
(def-theorem sb->gt2-obl-6
"forall(v:[ind_2,ind_1],u:[ind_1,ind_2],b:sets[ind_2],a:sets[ind_1],
nonempty_indic_q{a}
and
nonempty_indic_q{b}
and
dom{u}=a
and
dom{v}=b
and
ran{u} subseteq b
and
ran{v} subseteq a
and
injective_on_q{u,a}
and
injective_on_q{v,b}
implies
forall(x_1,x_2:ind_2,
x_1 in b and x_2 in b
implies
(v(x_1)=v(x_2) implies x_1=x_2)))"
lemma
(theory generic-theory-2)
(proof
(
direct-and-antecedent-inference-strategy
(backchain "with(v:[ind_2,ind_1],b:sets[ind_2],injective_on_q{v,b})")
direct-inference
)))
```