This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )