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

Metamath Proof Explorer

Theorem rinvf1o

Description: Sufficient conditions for the restriction of an involution to be a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Hypotheses rinvbij.1 
|- Fun F
rinvbij.2 
|- `' F = F
rinvbij.3a 
|- ( F " A ) C_ B
rinvbij.3b 
|- ( F " B ) C_ A
rinvbij.4a 
|- A C_ dom F
rinvbij.4b 
|- B C_ dom F
Assertion rinvf1o 
|- ( F |` A ) : A -1-1-onto-> B

Proof

Step Hyp Ref Expression
1 rinvbij.1 
 |-  Fun F
2 rinvbij.2 
 |-  `' F = F
3 rinvbij.3a 
 |-  ( F " A ) C_ B
4 rinvbij.3b 
 |-  ( F " B ) C_ A
5 rinvbij.4a 
 |-  A C_ dom F
6 rinvbij.4b 
 |-  B C_ dom F
7 fdmrn 
 |-  ( Fun F <-> F : dom F --> ran F )
8 1 7 mpbi 
 |-  F : dom F --> ran F
9 2 funeqi 
 |-  ( Fun `' F <-> Fun F )
10 1 9 mpbir 
 |-  Fun `' F
11 df-f1 
 |-  ( F : dom F -1-1-> ran F <-> ( F : dom F --> ran F /\ Fun `' F ) )
12 8 10 11 mpbir2an 
 |-  F : dom F -1-1-> ran F
13 f1ores 
 |-  ( ( F : dom F -1-1-> ran F /\ A C_ dom F ) -> ( F |` A ) : A -1-1-onto-> ( F " A ) )
14 12 5 13 mp2an 
 |-  ( F |` A ) : A -1-1-onto-> ( F " A )
15 funimass3 
 |-  ( ( Fun F /\ B C_ dom F ) -> ( ( F " B ) C_ A <-> B C_ ( `' F " A ) ) )
16 1 6 15 mp2an 
 |-  ( ( F " B ) C_ A <-> B C_ ( `' F " A ) )
17 4 16 mpbi 
 |-  B C_ ( `' F " A )
18 2 imaeq1i 
 |-  ( `' F " A ) = ( F " A )
19 17 18 sseqtri 
 |-  B C_ ( F " A )
20 3 19 eqssi 
 |-  ( F " A ) = B
21 f1oeq3 
 |-  ( ( F " A ) = B -> ( ( F |` A ) : A -1-1-onto-> ( F " A ) <-> ( F |` A ) : A -1-1-onto-> B ) )
22 20 21 ax-mp 
 |-  ( ( F |` A ) : A -1-1-onto-> ( F " A ) <-> ( F |` A ) : A -1-1-onto-> B )
23 14 22 mpbi 
 |-  ( F |` A ) : A -1-1-onto-> B