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