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

Metamath Proof Explorer

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