# Metamath Proof Explorer

## Theorem sbthlem10

Description: Lemma for sbth . (Contributed by NM, 28-Mar-1998)

Ref Expression
Hypotheses sbthlem.1 ${⊢}{A}\in \mathrm{V}$
sbthlem.2 ${⊢}{D}=\left\{{x}|\left({x}\subseteq {A}\wedge {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\right)\right\}$
sbthlem.3 ${⊢}{H}=\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
sbthlem.4 ${⊢}{B}\in \mathrm{V}$
Assertion sbthlem10 ${⊢}\left({A}\preccurlyeq {B}\wedge {B}\preccurlyeq {A}\right)\to {A}\approx {B}$

### Proof

Step Hyp Ref Expression
1 sbthlem.1 ${⊢}{A}\in \mathrm{V}$
2 sbthlem.2 ${⊢}{D}=\left\{{x}|\left({x}\subseteq {A}\wedge {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\right)\right\}$
3 sbthlem.3 ${⊢}{H}=\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
4 sbthlem.4 ${⊢}{B}\in \mathrm{V}$
5 4 brdom ${⊢}{A}\preccurlyeq {B}↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1}{⟶}{B}$
6 1 brdom ${⊢}{B}\preccurlyeq {A}↔\exists {g}\phantom{\rule{.4em}{0ex}}{g}:{B}\underset{1-1}{⟶}{A}$
7 5 6 anbi12i ${⊢}\left({A}\preccurlyeq {B}\wedge {B}\preccurlyeq {A}\right)↔\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1}{⟶}{B}\wedge \exists {g}\phantom{\rule{.4em}{0ex}}{g}:{B}\underset{1-1}{⟶}{A}\right)$
8 exdistrv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)↔\left(\exists {f}\phantom{\rule{.4em}{0ex}}{f}:{A}\underset{1-1}{⟶}{B}\wedge \exists {g}\phantom{\rule{.4em}{0ex}}{g}:{B}\underset{1-1}{⟶}{A}\right)$
9 7 8 bitr4i ${⊢}\left({A}\preccurlyeq {B}\wedge {B}\preccurlyeq {A}\right)↔\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)$
10 vex ${⊢}{f}\in \mathrm{V}$
11 10 resex ${⊢}{{f}↾}_{\bigcup {D}}\in \mathrm{V}$
12 vex ${⊢}{g}\in \mathrm{V}$
13 12 cnvex ${⊢}{{g}}^{-1}\in \mathrm{V}$
14 13 resex ${⊢}{{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\in \mathrm{V}$
15 11 14 unex ${⊢}\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\in \mathrm{V}$
16 3 15 eqeltri ${⊢}{H}\in \mathrm{V}$
17 1 2 3 sbthlem9 ${⊢}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)\to {H}:{A}\underset{1-1 onto}{⟶}{B}$
18 f1oen3g ${⊢}\left({H}\in \mathrm{V}\wedge {H}:{A}\underset{1-1 onto}{⟶}{B}\right)\to {A}\approx {B}$
19 16 17 18 sylancr ${⊢}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)\to {A}\approx {B}$
20 19 exlimivv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}\exists {g}\phantom{\rule{.4em}{0ex}}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)\to {A}\approx {B}$
21 9 20 sylbi ${⊢}\left({A}\preccurlyeq {B}\wedge {B}\preccurlyeq {A}\right)\to {A}\approx {B}$