# Metamath Proof Explorer

## Theorem sbthlem9

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)$
Assertion sbthlem9 ${⊢}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)\to {H}:{A}\underset{1-1 onto}{⟶}{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 1 2 3 sbthlem7 ${⊢}\left(\mathrm{Fun}{f}\wedge \mathrm{Fun}{{g}}^{-1}\right)\to \mathrm{Fun}{H}$
5 1 2 3 sbthlem5 ${⊢}\left(\mathrm{dom}{f}={A}\wedge \mathrm{ran}{g}\subseteq {A}\right)\to \mathrm{dom}{H}={A}$
6 5 adantrl ${⊢}\left(\mathrm{dom}{f}={A}\wedge \left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\right)\to \mathrm{dom}{H}={A}$
7 4 6 anim12i ${⊢}\left(\left(\mathrm{Fun}{f}\wedge \mathrm{Fun}{{g}}^{-1}\right)\wedge \left(\mathrm{dom}{f}={A}\wedge \left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\right)\right)\to \left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)$
8 7 an42s ${⊢}\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)$
9 8 adantlr ${⊢}\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)$
10 9 adantlr ${⊢}\left(\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \mathrm{Fun}{{f}}^{-1}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)$
11 1 2 3 sbthlem8 ${⊢}\left(\mathrm{Fun}{{f}}^{-1}\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \mathrm{Fun}{{H}}^{-1}$
12 11 adantll ${⊢}\left(\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \mathrm{Fun}{{f}}^{-1}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \mathrm{Fun}{{H}}^{-1}$
13 simpr ${⊢}\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\to \mathrm{dom}{g}={B}$
14 13 anim1i ${⊢}\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\to \left(\mathrm{dom}{g}={B}\wedge \mathrm{ran}{g}\subseteq {A}\right)$
15 df-rn ${⊢}\mathrm{ran}{H}=\mathrm{dom}{{H}}^{-1}$
16 1 2 3 sbthlem6 ${⊢}\left(\mathrm{ran}{f}\subseteq {B}\wedge \left(\left(\mathrm{dom}{g}={B}\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \mathrm{ran}{H}={B}$
17 15 16 syl5eqr ${⊢}\left(\mathrm{ran}{f}\subseteq {B}\wedge \left(\left(\mathrm{dom}{g}={B}\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \mathrm{dom}{{H}}^{-1}={B}$
18 14 17 sylanr1 ${⊢}\left(\mathrm{ran}{f}\subseteq {B}\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \mathrm{dom}{{H}}^{-1}={B}$
19 18 adantll ${⊢}\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \mathrm{dom}{{H}}^{-1}={B}$
20 19 adantlr ${⊢}\left(\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \mathrm{Fun}{{f}}^{-1}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \mathrm{dom}{{H}}^{-1}={B}$
21 10 12 20 jca32 ${⊢}\left(\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \mathrm{Fun}{{f}}^{-1}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to \left(\left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)\wedge \left(\mathrm{Fun}{{H}}^{-1}\wedge \mathrm{dom}{{H}}^{-1}={B}\right)\right)$
22 df-f1 ${⊢}{f}:{A}\underset{1-1}{⟶}{B}↔\left({f}:{A}⟶{B}\wedge \mathrm{Fun}{{f}}^{-1}\right)$
23 df-f ${⊢}{f}:{A}⟶{B}↔\left({f}Fn{A}\wedge \mathrm{ran}{f}\subseteq {B}\right)$
24 df-fn ${⊢}{f}Fn{A}↔\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)$
25 24 anbi1i ${⊢}\left({f}Fn{A}\wedge \mathrm{ran}{f}\subseteq {B}\right)↔\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)$
26 23 25 bitri ${⊢}{f}:{A}⟶{B}↔\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)$
27 26 anbi1i ${⊢}\left({f}:{A}⟶{B}\wedge \mathrm{Fun}{{f}}^{-1}\right)↔\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \mathrm{Fun}{{f}}^{-1}\right)$
28 22 27 bitri ${⊢}{f}:{A}\underset{1-1}{⟶}{B}↔\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \mathrm{Fun}{{f}}^{-1}\right)$
29 df-f1 ${⊢}{g}:{B}\underset{1-1}{⟶}{A}↔\left({g}:{B}⟶{A}\wedge \mathrm{Fun}{{g}}^{-1}\right)$
30 df-f ${⊢}{g}:{B}⟶{A}↔\left({g}Fn{B}\wedge \mathrm{ran}{g}\subseteq {A}\right)$
31 df-fn ${⊢}{g}Fn{B}↔\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)$
32 31 anbi1i ${⊢}\left({g}Fn{B}\wedge \mathrm{ran}{g}\subseteq {A}\right)↔\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)$
33 30 32 bitri ${⊢}{g}:{B}⟶{A}↔\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)$
34 33 anbi1i ${⊢}\left({g}:{B}⟶{A}\wedge \mathrm{Fun}{{g}}^{-1}\right)↔\left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)$
35 29 34 bitri ${⊢}{g}:{B}\underset{1-1}{⟶}{A}↔\left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)$
36 28 35 anbi12i ${⊢}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)↔\left(\left(\left(\left(\mathrm{Fun}{f}\wedge \mathrm{dom}{f}={A}\right)\wedge \mathrm{ran}{f}\subseteq {B}\right)\wedge \mathrm{Fun}{{f}}^{-1}\right)\wedge \left(\left(\left(\mathrm{Fun}{g}\wedge \mathrm{dom}{g}={B}\right)\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)$
37 dff1o4 ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}↔\left({H}Fn{A}\wedge {{H}}^{-1}Fn{B}\right)$
38 df-fn ${⊢}{H}Fn{A}↔\left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)$
39 df-fn ${⊢}{{H}}^{-1}Fn{B}↔\left(\mathrm{Fun}{{H}}^{-1}\wedge \mathrm{dom}{{H}}^{-1}={B}\right)$
40 38 39 anbi12i ${⊢}\left({H}Fn{A}\wedge {{H}}^{-1}Fn{B}\right)↔\left(\left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)\wedge \left(\mathrm{Fun}{{H}}^{-1}\wedge \mathrm{dom}{{H}}^{-1}={B}\right)\right)$
41 37 40 bitri ${⊢}{H}:{A}\underset{1-1 onto}{⟶}{B}↔\left(\left(\mathrm{Fun}{H}\wedge \mathrm{dom}{H}={A}\right)\wedge \left(\mathrm{Fun}{{H}}^{-1}\wedge \mathrm{dom}{{H}}^{-1}={B}\right)\right)$
42 21 36 41 3imtr4i ${⊢}\left({f}:{A}\underset{1-1}{⟶}{B}\wedge {g}:{B}\underset{1-1}{⟶}{A}\right)\to {H}:{A}\underset{1-1 onto}{⟶}{B}$