# Metamath Proof Explorer

## Theorem sbthlem1

Description: Lemma for sbth . (Contributed by NM, 22-Mar-1998)

Ref Expression
Hypotheses sbthlem.1
`|- A e. _V`
sbthlem.2
`|- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }`
Assertion sbthlem1
`|- U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) )`

### Proof

Step Hyp Ref Expression
1 sbthlem.1
` |-  A e. _V`
2 sbthlem.2
` |-  D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) }`
3 unissb
` |-  ( U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) <-> A. x e. D x C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) )`
4 2 abeq2i
` |-  ( x e. D <-> ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) )`
5 difss2
` |-  ( ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) -> ( g " ( B \ ( f " x ) ) ) C_ A )`
6 ssconb
` |-  ( ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ A ) -> ( x C_ ( A \ ( g " ( B \ ( f " x ) ) ) ) <-> ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) )`
7 6 exbiri
` |-  ( x C_ A -> ( ( g " ( B \ ( f " x ) ) ) C_ A -> ( ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) -> x C_ ( A \ ( g " ( B \ ( f " x ) ) ) ) ) ) )`
8 5 7 syl5
` |-  ( x C_ A -> ( ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) -> ( ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) -> x C_ ( A \ ( g " ( B \ ( f " x ) ) ) ) ) ) )`
9 8 pm2.43d
` |-  ( x C_ A -> ( ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) -> x C_ ( A \ ( g " ( B \ ( f " x ) ) ) ) ) )`
10 9 imp
` |-  ( ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) -> x C_ ( A \ ( g " ( B \ ( f " x ) ) ) ) )`
11 4 10 sylbi
` |-  ( x e. D -> x C_ ( A \ ( g " ( B \ ( f " x ) ) ) ) )`
12 elssuni
` |-  ( x e. D -> x C_ U. D )`
13 imass2
` |-  ( x C_ U. D -> ( f " x ) C_ ( f " U. D ) )`
14 sscon
` |-  ( ( f " x ) C_ ( f " U. D ) -> ( B \ ( f " U. D ) ) C_ ( B \ ( f " x ) ) )`
15 12 13 14 3syl
` |-  ( x e. D -> ( B \ ( f " U. D ) ) C_ ( B \ ( f " x ) ) )`
16 imass2
` |-  ( ( B \ ( f " U. D ) ) C_ ( B \ ( f " x ) ) -> ( g " ( B \ ( f " U. D ) ) ) C_ ( g " ( B \ ( f " x ) ) ) )`
17 sscon
` |-  ( ( g " ( B \ ( f " U. D ) ) ) C_ ( g " ( B \ ( f " x ) ) ) -> ( A \ ( g " ( B \ ( f " x ) ) ) ) C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) )`
18 15 16 17 3syl
` |-  ( x e. D -> ( A \ ( g " ( B \ ( f " x ) ) ) ) C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) )`
19 11 18 sstrd
` |-  ( x e. D -> x C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) ) )`
20 3 19 mprgbir
` |-  U. D C_ ( A \ ( g " ( B \ ( f " U. D ) ) ) )`