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 FunF-1FA:AontoCFB:BontoDFAB:AB1-1 ontoCD

Proof

Step Hyp Ref Expression
1 resdif FunF-1FA:AontoCFB:BontoDFAB:AB1-1 ontoCD
2 f1ofo FAB:AB1-1 ontoCDFAB:ABontoCD
3 1 2 syl FunF-1FA:AontoCFB:BontoDFAB:ABontoCD
4 resdif FunF-1FA:AontoCFAB:ABontoCDFAAB:AAB1-1 ontoCCD
5 3 4 syld3an3 FunF-1FA:AontoCFB:BontoDFAAB:AAB1-1 ontoCCD
6 dfin4 CD=CCD
7 f1oeq3 CD=CCDFAB:AB1-1 ontoCDFAB:AB1-1 ontoCCD
8 6 7 ax-mp FAB:AB1-1 ontoCDFAB:AB1-1 ontoCCD
9 dfin4 AB=AAB
10 f1oeq2 AB=AABFAB:AB1-1 ontoCCDFAB:AAB1-1 ontoCCD
11 9 10 ax-mp FAB:AB1-1 ontoCCDFAB:AAB1-1 ontoCCD
12 9 reseq2i FAB=FAAB
13 f1oeq1 FAB=FAABFAB:AAB1-1 ontoCCDFAAB:AAB1-1 ontoCCD
14 12 13 ax-mp FAB:AAB1-1 ontoCCDFAAB:AAB1-1 ontoCCD
15 8 11 14 3bitrri FAAB:AAB1-1 ontoCCDFAB:AB1-1 ontoCD
16 5 15 sylib FunF-1FA:AontoCFB:BontoDFAB:AB1-1 ontoCD