Metamath Proof Explorer

Theorem fresf1o

Description: Conditions for a restriction to be a one-to-one onto function. (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Assertion fresf1o 
|- ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun ( `' F |` C ) <-> ( `' F |` C ) Fn dom ( `' F |` C ) )
2 1 biimpi 
 |-  ( Fun ( `' F |` C ) -> ( `' F |` C ) Fn dom ( `' F |` C ) )
3 2 3ad2ant3 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( `' F |` C ) Fn dom ( `' F |` C ) )
4 simp2 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> C C_ ran F )
5 df-rn 
 |-  ran F = dom `' F
6 4 5 sseqtrdi 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> C C_ dom `' F )
7 ssdmres 
 |-  ( C C_ dom `' F <-> dom ( `' F |` C ) = C )
8 6 7 sylib 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> dom ( `' F |` C ) = C )
9 8 fneq2d 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( ( `' F |` C ) Fn dom ( `' F |` C ) <-> ( `' F |` C ) Fn C ) )
10 3 9 mpbid 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( `' F |` C ) Fn C )
11 simp1 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> Fun F )
12 funres 
 |-  ( Fun F -> Fun ( F |` ( `' F " C ) ) )
13 11 12 syl 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> Fun ( F |` ( `' F " C ) ) )
14 funcnvres2 
 |-  ( Fun F -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
15 11 14 syl 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
16 15 funeqd 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( Fun `' ( `' F |` C ) <-> Fun ( F |` ( `' F " C ) ) ) )
17 13 16 mpbird 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> Fun `' ( `' F |` C ) )
18 df-ima 
 |-  ( `' F " C ) = ran ( `' F |` C )
19 18 eqcomi 
 |-  ran ( `' F |` C ) = ( `' F " C )
20 19 a1i 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ran ( `' F |` C ) = ( `' F " C ) )
21 dff1o2 
 |-  ( ( `' F |` C ) : C -1-1-onto-> ( `' F " C ) <-> ( ( `' F |` C ) Fn C /\ Fun `' ( `' F |` C ) /\ ran ( `' F |` C ) = ( `' F " C ) ) )
22 10 17 20 21 syl3anbrc 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( `' F |` C ) : C -1-1-onto-> ( `' F " C ) )
23 f1ocnv 
 |-  ( ( `' F |` C ) : C -1-1-onto-> ( `' F " C ) -> `' ( `' F |` C ) : ( `' F " C ) -1-1-onto-> C )
24 22 23 syl 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> `' ( `' F |` C ) : ( `' F " C ) -1-1-onto-> C )
25 f1oeq1 
 |-  ( `' ( `' F |` C ) = ( F |` ( `' F " C ) ) -> ( `' ( `' F |` C ) : ( `' F " C ) -1-1-onto-> C <-> ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-onto-> C ) )
26 11 14 25 3syl 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( `' ( `' F |` C ) : ( `' F " C ) -1-1-onto-> C <-> ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-onto-> C ) )
27 24 26 mpbid 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-onto-> C )