Metamath Proof Explorer

Theorem resdif

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

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

Proof

Step Hyp Ref Expression
1 fofun 
 |-  ( ( F |` A ) : A -onto-> C -> Fun ( F |` A ) )
2 difss 
 |-  ( A \ B ) C_ A
3 fof 
 |-  ( ( F |` A ) : A -onto-> C -> ( F |` A ) : A --> C )
4 3 fdmd 
 |-  ( ( F |` A ) : A -onto-> C -> dom ( F |` A ) = A )
5 2 4 sseqtrrid 
 |-  ( ( F |` A ) : A -onto-> C -> ( A \ B ) C_ dom ( F |` A ) )
6 fores 
 |-  ( ( Fun ( F |` A ) /\ ( A \ B ) C_ dom ( F |` A ) ) -> ( ( F |` A ) |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) )
7 1 5 6 syl2anc 
 |-  ( ( F |` A ) : A -onto-> C -> ( ( F |` A ) |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) )
8 resres 
 |-  ( ( F |` A ) |` ( A \ B ) ) = ( F |` ( A i^i ( A \ B ) ) )
9 indif 
 |-  ( A i^i ( A \ B ) ) = ( A \ B )
10 9 reseq2i 
 |-  ( F |` ( A i^i ( A \ B ) ) ) = ( F |` ( A \ B ) )
11 8 10 eqtri 
 |-  ( ( F |` A ) |` ( A \ B ) ) = ( F |` ( A \ B ) )
12 foeq1 
 |-  ( ( ( F |` A ) |` ( A \ B ) ) = ( F |` ( A \ B ) ) -> ( ( ( F |` A ) |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) <-> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) ) )
13 11 12 ax-mp 
 |-  ( ( ( F |` A ) |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) <-> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) )
14 11 rneqi 
 |-  ran ( ( F |` A ) |` ( A \ B ) ) = ran ( F |` ( A \ B ) )
15 df-ima 
 |-  ( ( F |` A ) " ( A \ B ) ) = ran ( ( F |` A ) |` ( A \ B ) )
16 df-ima 
 |-  ( F " ( A \ B ) ) = ran ( F |` ( A \ B ) )
17 14 15 16 3eqtr4i 
 |-  ( ( F |` A ) " ( A \ B ) ) = ( F " ( A \ B ) )
18 foeq3 
 |-  ( ( ( F |` A ) " ( A \ B ) ) = ( F " ( A \ B ) ) -> ( ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) <-> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( F " ( A \ B ) ) ) )
19 17 18 ax-mp 
 |-  ( ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) <-> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( F " ( A \ B ) ) )
20 13 19 bitri 
 |-  ( ( ( F |` A ) |` ( A \ B ) ) : ( A \ B ) -onto-> ( ( F |` A ) " ( A \ B ) ) <-> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( F " ( A \ B ) ) )
21 7 20 sylib 
 |-  ( ( F |` A ) : A -onto-> C -> ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( F " ( A \ B ) ) )
22 funres11 
 |-  ( Fun `' F -> Fun `' ( F |` ( A \ B ) ) )
23 dff1o3 
 |-  ( ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( F " ( A \ B ) ) <-> ( ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( F " ( A \ B ) ) /\ Fun `' ( F |` ( A \ B ) ) ) )
24 23 biimpri 
 |-  ( ( ( F |` ( A \ B ) ) : ( A \ B ) -onto-> ( F " ( A \ B ) ) /\ Fun `' ( F |` ( A \ B ) ) ) -> ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( F " ( A \ B ) ) )
25 21 22 24 syl2anr 
 |-  ( ( Fun `' F /\ ( F |` A ) : A -onto-> C ) -> ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( F " ( A \ B ) ) )
26 25 3adant3 
 |-  ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( F " ( A \ B ) ) )
27 df-ima 
 |-  ( F " A ) = ran ( F |` A )
28 forn 
 |-  ( ( F |` A ) : A -onto-> C -> ran ( F |` A ) = C )
29 27 28 syl5eq 
 |-  ( ( F |` A ) : A -onto-> C -> ( F " A ) = C )
30 df-ima 
 |-  ( F " B ) = ran ( F |` B )
31 forn 
 |-  ( ( F |` B ) : B -onto-> D -> ran ( F |` B ) = D )
32 30 31 syl5eq 
 |-  ( ( F |` B ) : B -onto-> D -> ( F " B ) = D )
33 29 32 anim12i 
 |-  ( ( ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( ( F " A ) = C /\ ( F " B ) = D ) )
34 imadif 
 |-  ( Fun `' F -> ( F " ( A \ B ) ) = ( ( F " A ) \ ( F " B ) ) )
35 difeq12 
 |-  ( ( ( F " A ) = C /\ ( F " B ) = D ) -> ( ( F " A ) \ ( F " B ) ) = ( C \ D ) )
36 34 35 sylan9eq 
 |-  ( ( Fun `' F /\ ( ( F " A ) = C /\ ( F " B ) = D ) ) -> ( F " ( A \ B ) ) = ( C \ D ) )
37 33 36 sylan2 
 |-  ( ( Fun `' F /\ ( ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) ) -> ( F " ( A \ B ) ) = ( C \ D ) )
38 37 3impb 
 |-  ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F " ( A \ B ) ) = ( C \ D ) )
39 38 f1oeq3d 
 |-  ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( F " ( A \ B ) ) <-> ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( C \ D ) ) )
40 26 39 mpbid 
 |-  ( ( Fun `' F /\ ( F |` A ) : A -onto-> C /\ ( F |` B ) : B -onto-> D ) -> ( F |` ( A \ B ) ) : ( A \ B ) -1-1-onto-> ( C \ D ) )