Theorem sbthlem6

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 ) ) }
	sbthlem.3	|- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
Assertion	sbthlem6	|- ( ( ran f C_ B /\ ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) ) -> ran H = B )

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		sbthlem.3	|- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
4		rnun	|- ran ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) = ( ran ( f |` U. D ) u. ran ( `' g |` ( A \ U. D ) ) )
5	3	rneqi	|- ran H = ran ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) )
6		df-ima	|- ( f " U. D ) = ran ( f |` U. D )
7	6	uneq1i	|- ( ( f " U. D ) u. ran ( `' g |` ( A \ U. D ) ) ) = ( ran ( f |` U. D ) u. ran ( `' g |` ( A \ U. D ) ) )
8	4 5 7	3eqtr4i	|- ran H = ( ( f " U. D ) u. ran ( `' g |` ( A \ U. D ) ) )
9	1 2	sbthlem4	|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( `' g " ( A \ U. D ) ) = ( B \ ( f " U. D ) ) )
10		df-ima	|- ( `' g " ( A \ U. D ) ) = ran ( `' g |` ( A \ U. D ) )
11	9 10	eqtr3di	|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( B \ ( f " U. D ) ) = ran ( `' g |` ( A \ U. D ) ) )
12	11	uneq2d	|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) = ( ( f " U. D ) u. ran ( `' g |` ( A \ U. D ) ) ) )
13	8 12	eqtr4id	|- ( ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) -> ran H = ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) )
14		imassrn	|- ( f " U. D ) C_ ran f
15		sstr2	|- ( ( f " U. D ) C_ ran f -> ( ran f C_ B -> ( f " U. D ) C_ B ) )
16	14 15	ax-mp	|- ( ran f C_ B -> ( f " U. D ) C_ B )
17		undif	|- ( ( f " U. D ) C_ B <-> ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) = B )
18	16 17	sylib	|- ( ran f C_ B -> ( ( f " U. D ) u. ( B \ ( f " U. D ) ) ) = B )
19	13 18	sylan9eqr	|- ( ( ran f C_ B /\ ( ( dom g = B /\ ran g C_ A ) /\ Fun `' g ) ) -> ran H = B )