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 11 funresd 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> Fun ( F |` ( `' F " C ) ) )
13 funcnvres2 
 |-  ( Fun F -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
14 11 13 syl 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
15 14 funeqd 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( Fun `' ( `' F |` C ) <-> Fun ( F |` ( `' F " C ) ) ) )
16 12 15 mpbird 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> Fun `' ( `' F |` C ) )
17 df-ima 
 |-  ( `' F " C ) = ran ( `' F |` C )
18 17 eqcomi 
 |-  ran ( `' F |` C ) = ( `' F " C )
19 18 a1i 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ran ( `' F |` C ) = ( `' F " C ) )
20 dff1o2 
 |-  ( ( `' F |` C ) : C -1-1-onto-> ( `' F " C ) <-> ( ( `' F |` C ) Fn C /\ Fun `' ( `' F |` C ) /\ ran ( `' F |` C ) = ( `' F " C ) ) )
21 10 16 19 20 syl3anbrc 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( `' F |` C ) : C -1-1-onto-> ( `' F " C ) )
22 f1ocnv 
 |-  ( ( `' F |` C ) : C -1-1-onto-> ( `' F " C ) -> `' ( `' F |` C ) : ( `' F " C ) -1-1-onto-> C )
23 21 22 syl 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> `' ( `' F |` C ) : ( `' F " C ) -1-1-onto-> C )
24 f1oeq1 
 |-  ( `' ( `' F |` C ) = ( F |` ( `' F " C ) ) -> ( `' ( `' F |` C ) : ( `' F " C ) -1-1-onto-> C <-> ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-onto-> C ) )
25 11 13 24 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 ) )
26 23 25 mpbid 
 |-  ( ( Fun F /\ C C_ ran F /\ Fun ( `' F |` C ) ) -> ( F |` ( `' F " C ) ) : ( `' F " C ) -1-1-onto-> C )