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

Metamath Proof Explorer

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 )