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