# Metamath Proof Explorer

## Theorem sbthlem5

Description: Lemma for sbth . (Contributed by NM, 22-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 sbthlem5 ${⊢}\left(\mathrm{dom}{f}={A}\wedge \mathrm{ran}{g}\subseteq {A}\right)\to \mathrm{dom}{H}={A}$

### 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 3 dmeqi ${⊢}\mathrm{dom}{H}=\mathrm{dom}\left(\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\right)$
5 dmun ${⊢}\mathrm{dom}\left(\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\right)=\mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cup \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
6 dmres ${⊢}\mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)=\bigcup {D}\cap \mathrm{dom}{f}$
7 dmres ${⊢}\mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)=\left({A}\setminus \bigcup {D}\right)\cap \mathrm{dom}{{g}}^{-1}$
8 df-rn ${⊢}\mathrm{ran}{g}=\mathrm{dom}{{g}}^{-1}$
9 8 eqcomi ${⊢}\mathrm{dom}{{g}}^{-1}=\mathrm{ran}{g}$
10 9 ineq2i ${⊢}\left({A}\setminus \bigcup {D}\right)\cap \mathrm{dom}{{g}}^{-1}=\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}$
11 7 10 eqtri ${⊢}\mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)=\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}$
12 6 11 uneq12i ${⊢}\mathrm{dom}\left({{f}↾}_{\bigcup {D}}\right)\cup \mathrm{dom}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)=\left(\bigcup {D}\cap \mathrm{dom}{f}\right)\cup \left(\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}\right)$
13 5 12 eqtri ${⊢}\mathrm{dom}\left(\left({{f}↾}_{\bigcup {D}}\right)\cup \left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)\right)=\left(\bigcup {D}\cap \mathrm{dom}{f}\right)\cup \left(\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}\right)$
14 4 13 eqtri ${⊢}\mathrm{dom}{H}=\left(\bigcup {D}\cap \mathrm{dom}{f}\right)\cup \left(\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}\right)$
15 1 2 sbthlem1 ${⊢}\bigcup {D}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
16 difss ${⊢}{A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq {A}$
17 15 16 sstri ${⊢}\bigcup {D}\subseteq {A}$
18 sseq2 ${⊢}\mathrm{dom}{f}={A}\to \left(\bigcup {D}\subseteq \mathrm{dom}{f}↔\bigcup {D}\subseteq {A}\right)$
19 17 18 mpbiri ${⊢}\mathrm{dom}{f}={A}\to \bigcup {D}\subseteq \mathrm{dom}{f}$
20 dfss ${⊢}\bigcup {D}\subseteq \mathrm{dom}{f}↔\bigcup {D}=\bigcup {D}\cap \mathrm{dom}{f}$
21 19 20 sylib ${⊢}\mathrm{dom}{f}={A}\to \bigcup {D}=\bigcup {D}\cap \mathrm{dom}{f}$
22 21 uneq1d ${⊢}\mathrm{dom}{f}={A}\to \bigcup {D}\cup \left({A}\setminus \bigcup {D}\right)=\left(\bigcup {D}\cap \mathrm{dom}{f}\right)\cup \left({A}\setminus \bigcup {D}\right)$
23 1 2 sbthlem3 ${⊢}\mathrm{ran}{g}\subseteq {A}\to {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]={A}\setminus \bigcup {D}$
24 imassrn ${⊢}{g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq \mathrm{ran}{g}$
25 23 24 eqsstrrdi ${⊢}\mathrm{ran}{g}\subseteq {A}\to {A}\setminus \bigcup {D}\subseteq \mathrm{ran}{g}$
26 dfss ${⊢}{A}\setminus \bigcup {D}\subseteq \mathrm{ran}{g}↔{A}\setminus \bigcup {D}=\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}$
27 25 26 sylib ${⊢}\mathrm{ran}{g}\subseteq {A}\to {A}\setminus \bigcup {D}=\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}$
28 27 uneq2d ${⊢}\mathrm{ran}{g}\subseteq {A}\to \left(\bigcup {D}\cap \mathrm{dom}{f}\right)\cup \left({A}\setminus \bigcup {D}\right)=\left(\bigcup {D}\cap \mathrm{dom}{f}\right)\cup \left(\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}\right)$
29 22 28 sylan9eq ${⊢}\left(\mathrm{dom}{f}={A}\wedge \mathrm{ran}{g}\subseteq {A}\right)\to \bigcup {D}\cup \left({A}\setminus \bigcup {D}\right)=\left(\bigcup {D}\cap \mathrm{dom}{f}\right)\cup \left(\left({A}\setminus \bigcup {D}\right)\cap \mathrm{ran}{g}\right)$
30 14 29 eqtr4id ${⊢}\left(\mathrm{dom}{f}={A}\wedge \mathrm{ran}{g}\subseteq {A}\right)\to \mathrm{dom}{H}=\bigcup {D}\cup \left({A}\setminus \bigcup {D}\right)$
31 undif ${⊢}\bigcup {D}\subseteq {A}↔\bigcup {D}\cup \left({A}\setminus \bigcup {D}\right)={A}$
32 17 31 mpbi ${⊢}\bigcup {D}\cup \left({A}\setminus \bigcup {D}\right)={A}$
33 30 32 eqtrdi ${⊢}\left(\mathrm{dom}{f}={A}\wedge \mathrm{ran}{g}\subseteq {A}\right)\to \mathrm{dom}{H}={A}$