# Metamath Proof Explorer

## Theorem sbthlem3

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\}$
Assertion sbthlem3 ${⊢}\mathrm{ran}{g}\subseteq {A}\to {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]={A}\setminus \bigcup {D}$

### 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 1 2 sbthlem2 ${⊢}\mathrm{ran}{g}\subseteq {A}\to {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq \bigcup {D}$
4 1 2 sbthlem1 ${⊢}\bigcup {D}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
5 3 4 jctil ${⊢}\mathrm{ran}{g}\subseteq {A}\to \left(\bigcup {D}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\wedge {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq \bigcup {D}\right)$
6 eqss ${⊢}\bigcup {D}={A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]↔\left(\bigcup {D}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\wedge {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq \bigcup {D}\right)$
7 5 6 sylibr ${⊢}\mathrm{ran}{g}\subseteq {A}\to \bigcup {D}={A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
8 7 difeq2d ${⊢}\mathrm{ran}{g}\subseteq {A}\to {A}\setminus \bigcup {D}={A}\setminus \left({A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\right)$
9 imassrn ${⊢}{g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq \mathrm{ran}{g}$
10 sstr2 ${⊢}{g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq \mathrm{ran}{g}\to \left(\mathrm{ran}{g}\subseteq {A}\to {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq {A}\right)$
11 9 10 ax-mp ${⊢}\mathrm{ran}{g}\subseteq {A}\to {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq {A}$
12 dfss4 ${⊢}{g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq {A}↔{A}\setminus \left({A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\right)={g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
13 11 12 sylib ${⊢}\mathrm{ran}{g}\subseteq {A}\to {A}\setminus \left({A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\right)={g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
14 8 13 eqtr2d ${⊢}\mathrm{ran}{g}\subseteq {A}\to {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]={A}\setminus \bigcup {D}$