Theorem resin

Description: The restriction of a one-to-one onto function to an intersection maps onto the intersection of the images. (Contributed by Paul Chapman, 11-Apr-2009)

	Ref	Expression
Assertion	resin	|- ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C i^i D ) )

Proof

Step	Hyp	Ref	Expression
1		resdif	|- ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( C \ D ) )
2		f1ofo	|- ( ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( C \ D ) -> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( C \ D ) )
3	1 2	syl	|- ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( C \ D ) )
4		resdif	|- ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( C \ D ) ) -> ( F |` ( A \ ( A \ B ) ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) )
5	3 4	syld3an3	|- ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F |` ( A \ ( A \ B ) ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) )
6		dfin4	|- ( C i^i D ) = ( C \ ( C \ D ) )
7		f1oeq3	|- ( ( C i^i D ) = ( C \ ( C \ D ) ) -> ( ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C i^i D ) <-> ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C \ ( C \ D ) ) ) )
8	6 7	ax-mp	|- ( ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C i^i D ) <-> ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C \ ( C \ D ) ) )
9		dfin4	|- ( A i^i B ) = ( A \ ( A \ B ) )
10		f1oeq2	|- ( ( A i^i B ) = ( A \ ( A \ B ) ) -> ( ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C \ ( C \ D ) ) <-> ( F |` ( A i^i B ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) ) )
11	9 10	ax-mp	|- ( ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C \ ( C \ D ) ) <-> ( F |` ( A i^i B ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) )
12	9	reseq2i	|- ( F |` ( A i^i B ) ) = ( F |` ( A \ ( A \ B ) ) )
13		f1oeq1	|- ( ( F |` ( A i^i B ) ) = ( F |` ( A \ ( A \ B ) ) ) -> ( ( F |` ( A i^i B ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) <-> ( F |` ( A \ ( A \ B ) ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) ) )
14	12 13	ax-mp	|- ( ( F |` ( A i^i B ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) <-> ( F |` ( A \ ( A \ B ) ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) )
15	8 11 14	3bitrri	|- ( ( F |` ( A \ ( A \ B ) ) ) : ( A \ ( A \ B ) ) -1-1-onto-> ( C \ ( C \ D ) ) <-> ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C i^i D ) )
16	5 15	sylib	|- ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F |` ( A i^i B ) ) : ( A i^i B ) -1-1-onto-> ( C i^i D ) )