# Metamath Proof Explorer

## Theorem sbthlem1

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 sbthlem1 ${⊢}\bigcup {D}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\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 unissb ${⊢}\bigcup {D}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]↔\forall {x}\in {D}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
4 2 abeq2i ${⊢}{x}\in {D}↔\left({x}\subseteq {A}\wedge {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\right)$
5 difss2 ${⊢}{g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\to {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}$
6 ssconb ${⊢}\left({x}\subseteq {A}\wedge {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\right)\to \left({x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]↔{g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\right)$
7 6 exbiri ${⊢}{x}\subseteq {A}\to \left({g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\to \left({g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\to {x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]\right)\right)$
8 5 7 syl5 ${⊢}{x}\subseteq {A}\to \left({g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\to \left({g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\to {x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]\right)\right)$
9 8 pm2.43d ${⊢}{x}\subseteq {A}\to \left({g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\to {x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]\right)$
10 9 imp ${⊢}\left({x}\subseteq {A}\wedge {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {x}\right)\to {x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]$
11 4 10 sylbi ${⊢}{x}\in {D}\to {x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]$
12 elssuni ${⊢}{x}\in {D}\to {x}\subseteq \bigcup {D}$
13 imass2 ${⊢}{x}\subseteq \bigcup {D}\to {f}\left[{x}\right]\subseteq {f}\left[\bigcup {D}\right]$
14 sscon ${⊢}{f}\left[{x}\right]\subseteq {f}\left[\bigcup {D}\right]\to {B}\setminus {f}\left[\bigcup {D}\right]\subseteq {B}\setminus {f}\left[{x}\right]$
15 12 13 14 3syl ${⊢}{x}\in {D}\to {B}\setminus {f}\left[\bigcup {D}\right]\subseteq {B}\setminus {f}\left[{x}\right]$
16 imass2 ${⊢}{B}\setminus {f}\left[\bigcup {D}\right]\subseteq {B}\setminus {f}\left[{x}\right]\to {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq {g}\left[{B}\setminus {f}\left[{x}\right]\right]$
17 sscon ${⊢}{g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]\subseteq {g}\left[{B}\setminus {f}\left[{x}\right]\right]\to {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
18 15 16 17 3syl ${⊢}{x}\in {D}\to {A}\setminus {g}\left[{B}\setminus {f}\left[{x}\right]\right]\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
19 11 18 sstrd ${⊢}{x}\in {D}\to {x}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$
20 3 19 mprgbir ${⊢}\bigcup {D}\subseteq {A}\setminus {g}\left[{B}\setminus {f}\left[\bigcup {D}\right]\right]$