# Metamath Proof Explorer

## Theorem sbthlem4

Description: Lemma for sbth . (Contributed by NM, 27-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 sbthlem4
`|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( `' g " ( A \ U. D ) ) = ( 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 df-ima
` |-  ( `' g " ( A \ U. D ) ) = ran ( `' g |` ( A \ U. D ) )`
4 dfdm4
` |-  dom ( g |` ( B \ ( f " U. D ) ) ) = ran `' ( g |` ( B \ ( f " U. D ) ) )`
5 difss
` |-  ( B \ ( f " U. D ) ) C_ B`
6 sseq2
` |-  ( dom g = B -> ( ( B \ ( f " U. D ) ) C_ dom g <-> ( B \ ( f " U. D ) ) C_ B ) )`
7 5 6 mpbiri
` |-  ( dom g = B -> ( B \ ( f " U. D ) ) C_ dom g )`
8 ssdmres
` |-  ( ( B \ ( f " U. D ) ) C_ dom g <-> dom ( g |` ( B \ ( f " U. D ) ) ) = ( B \ ( f " U. D ) ) )`
9 7 8 sylib
` |-  ( dom g = B -> dom ( g |` ( B \ ( f " U. D ) ) ) = ( B \ ( f " U. D ) ) )`
10 4 9 syl5reqr
` |-  ( dom g = B -> ( B \ ( f " U. D ) ) = ran `' ( g |` ( B \ ( f " U. D ) ) ) )`
11 funcnvres
` |-  ( Fun `' g -> `' ( g |` ( B \ ( f " U. D ) ) ) = ( `' g |` ( g " ( B \ ( f " U. D ) ) ) ) )`
12 1 2 sbthlem3
` |-  ( ran g C_ A -> ( g " ( B \ ( f " U. D ) ) ) = ( A \ U. D ) )`
13 12 reseq2d
` |-  ( ran g C_ A -> ( `' g |` ( g " ( B \ ( f " U. D ) ) ) ) = ( `' g |` ( A \ U. D ) ) )`
14 11 13 sylan9eqr
` |-  ( ( ran g C_ A /\ Fun `' g ) -> `' ( g |` ( B \ ( f " U. D ) ) ) = ( `' g |` ( A \ U. D ) ) )`
15 14 rneqd
` |-  ( ( ran g C_ A /\ Fun `' g ) -> ran `' ( g |` ( B \ ( f " U. D ) ) ) = ran ( `' g |` ( A \ U. D ) ) )`
16 10 15 sylan9eq
` |-  ( ( dom g = B /\ ( ran g C_ A /\ Fun `' g ) ) -> ( B \ ( f " U. D ) ) = ran ( `' g |` ( A \ U. D ) ) )`
17 16 anassrs
` |-  ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( B \ ( f " U. D ) ) = ran ( `' g |` ( A \ U. D ) ) )`
18 3 17 eqtr4id
` |-  ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( `' g " ( A \ U. D ) ) = ( B \ ( f " U. D ) ) )`