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 difss
 |-  ( B \ ( f " U. D ) ) C_ B
5 sseq2
 |-  ( dom g = B -> ( ( B \ ( f " U. D ) ) C_ dom g <-> ( B \ ( f " U. D ) ) C_ B ) )
6 4 5 mpbiri
 |-  ( dom g = B -> ( B \ ( f " U. D ) ) C_ dom g )
7 ssdmres
 |-  ( ( B \ ( f " U. D ) ) C_ dom g <-> dom ( g |` ( B \ ( f " U. D ) ) ) = ( B \ ( f " U. D ) ) )
8 6 7 sylib
 |-  ( dom g = B -> dom ( g |` ( B \ ( f " U. D ) ) ) = ( B \ ( f " U. D ) ) )
9 dfdm4
 |-  dom ( g |` ( B \ ( f " U. D ) ) ) = ran `' ( g |` ( B \ ( f " U. D ) ) )
10 8 9 eqtr3di
 |-  ( 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 ) ) )