# Metamath Proof Explorer

## Theorem sbthlem4

Description: Lemma for sbth . (Contributed by NM, 27-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\}$
Assertion sbthlem4 ${⊢}\left(\left(\mathrm{dom}{g}={B}\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\to {{g}}^{-1}\left[{A}\setminus \bigcup {D}\right]={B}\setminus {f}\left[\bigcup {D}\right]$

### 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 dfdm4 ${⊢}\mathrm{dom}\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)=\mathrm{ran}{\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)}^{-1}$
4 difss ${⊢}{B}\setminus {f}\left[\bigcup {D}\right]\subseteq {B}$
5 sseq2 ${⊢}\mathrm{dom}{g}={B}\to \left({B}\setminus {f}\left[\bigcup {D}\right]\subseteq \mathrm{dom}{g}↔{B}\setminus {f}\left[\bigcup {D}\right]\subseteq {B}\right)$
6 4 5 mpbiri ${⊢}\mathrm{dom}{g}={B}\to {B}\setminus {f}\left[\bigcup {D}\right]\subseteq \mathrm{dom}{g}$
7 ssdmres ${⊢}{B}\setminus {f}\left[\bigcup {D}\right]\subseteq \mathrm{dom}{g}↔\mathrm{dom}\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)={B}\setminus {f}\left[\bigcup {D}\right]$
8 6 7 sylib ${⊢}\mathrm{dom}{g}={B}\to \mathrm{dom}\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)={B}\setminus {f}\left[\bigcup {D}\right]$
9 3 8 syl5reqr ${⊢}\mathrm{dom}{g}={B}\to {B}\setminus {f}\left[\bigcup {D}\right]=\mathrm{ran}{\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)}^{-1}$
10 funcnvres ${⊢}\mathrm{Fun}{{g}}^{-1}\to {\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)}^{-1}={{{g}}^{-1}↾}_{{g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]}$
11 1 2 sbthlem3 ${⊢}\mathrm{ran}{g}\subseteq {A}\to {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]={A}\setminus \bigcup {D}$
12 11 reseq2d ${⊢}\mathrm{ran}{g}\subseteq {A}\to {{{g}}^{-1}↾}_{{g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]}={{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}$
13 10 12 sylan9eqr ${⊢}\left(\mathrm{ran}{g}\subseteq {A}\wedge \mathrm{Fun}{{g}}^{-1}\right)\to {\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)}^{-1}={{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}$
14 13 rneqd ${⊢}\left(\mathrm{ran}{g}\subseteq {A}\wedge \mathrm{Fun}{{g}}^{-1}\right)\to \mathrm{ran}{\left({{g}↾}_{\left({B}\setminus {f}\left[\bigcup {D}\right]\right)}\right)}^{-1}=\mathrm{ran}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
15 9 14 sylan9eq ${⊢}\left(\mathrm{dom}{g}={B}\wedge \left(\mathrm{ran}{g}\subseteq {A}\wedge \mathrm{Fun}{{g}}^{-1}\right)\right)\to {B}\setminus {f}\left[\bigcup {D}\right]=\mathrm{ran}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
16 15 anassrs ${⊢}\left(\left(\mathrm{dom}{g}={B}\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\to {B}\setminus {f}\left[\bigcup {D}\right]=\mathrm{ran}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
17 df-ima ${⊢}{{g}}^{-1}\left[{A}\setminus \bigcup {D}\right]=\mathrm{ran}\left({{{g}}^{-1}↾}_{\left({A}\setminus \bigcup {D}\right)}\right)$
18 16 17 syl6reqr ${⊢}\left(\left(\mathrm{dom}{g}={B}\wedge \mathrm{ran}{g}\subseteq {A}\right)\wedge \mathrm{Fun}{{g}}^{-1}\right)\to {{g}}^{-1}\left[{A}\setminus \bigcup {D}\right]={B}\setminus {f}\left[\bigcup {D}\right]$