Theorem nvof1o

Description: An involution is a bijection. (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Assertion	nvof1o	|- ( ( F Fn A /\ `' F = F ) -> F : A -1-1-onto-> A )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( F Fn A -> Fun F )
2		fdmrn	|- ( Fun F <-> F : dom F --> ran F )
3	1 2	sylib	|- ( F Fn A -> F : dom F --> ran F )
4	3	adantr	|- ( ( F Fn A /\ `' F = F ) -> F : dom F --> ran F )
5		fndm	|- ( F Fn A -> dom F = A )
6	5	adantr	|- ( ( F Fn A /\ `' F = F ) -> dom F = A )
7		df-rn	|- ran F = dom `' F
8		dmeq	|- ( `' F = F -> dom `' F = dom F )
9	7 8	eqtrid	|- ( `' F = F -> ran F = dom F )
10	9 5	sylan9eqr	|- ( ( F Fn A /\ `' F = F ) -> ran F = A )
11	6 10	feq23d	|- ( ( F Fn A /\ `' F = F ) -> ( F : dom F --> ran F <-> F : A --> A ) )
12	4 11	mpbid	|- ( ( F Fn A /\ `' F = F ) -> F : A --> A )
13	1	adantr	|- ( ( F Fn A /\ `' F = F ) -> Fun F )
14		funeq	|- ( `' F = F -> ( Fun `' F <-> Fun F ) )
15	14	adantl	|- ( ( F Fn A /\ `' F = F ) -> ( Fun `' F <-> Fun F ) )
16	13 15	mpbird	|- ( ( F Fn A /\ `' F = F ) -> Fun `' F )
17		df-f1	|- ( F : A -1-1-> A <-> ( F : A --> A /\ Fun `' F ) )
18	12 16 17	sylanbrc	|- ( ( F Fn A /\ `' F = F ) -> F : A -1-1-> A )
19		simpl	|- ( ( F Fn A /\ `' F = F ) -> F Fn A )
20		df-fo	|- ( F : A -onto-> A <-> ( F Fn A /\ ran F = A ) )
21	19 10 20	sylanbrc	|- ( ( F Fn A /\ `' F = F ) -> F : A -onto-> A )
22		df-f1o	|- ( F : A -1-1-onto-> A <-> ( F : A -1-1-> A /\ F : A -onto-> A ) )
23	18 21 22	sylanbrc	|- ( ( F Fn A /\ `' F = F ) -> F : A -1-1-onto-> A )