Metamath Proof Explorer

Theorem f1omvdcnv

Description: A permutation and its inverse move the same points. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Assertion f1omvdcnv 
|- ( F : A -1-1-onto-> A -> dom ( `' F \ _I ) = dom ( F \ _I ) )

Proof

Step Hyp Ref Expression
1 f1ocnvfvb 
 |-  ( ( F : A -1-1-onto-> A /\ x e. A /\ x e. A ) -> ( ( F ` x ) = x <-> ( `' F ` x ) = x ) )
2 1 3anidm23 
 |-  ( ( F : A -1-1-onto-> A /\ x e. A ) -> ( ( F ` x ) = x <-> ( `' F ` x ) = x ) )
3 2 bicomd 
 |-  ( ( F : A -1-1-onto-> A /\ x e. A ) -> ( ( `' F ` x ) = x <-> ( F ` x ) = x ) )
4 3 necon3bid 
 |-  ( ( F : A -1-1-onto-> A /\ x e. A ) -> ( ( `' F ` x ) =/= x <-> ( F ` x ) =/= x ) )
5 4 rabbidva 
 |-  ( F : A -1-1-onto-> A -> { x e. A | ( `' F ` x ) =/= x } = { x e. A | ( F ` x ) =/= x } )
6 f1ocnv 
 |-  ( F : A -1-1-onto-> A -> `' F : A -1-1-onto-> A )
7 f1ofn 
 |-  ( `' F : A -1-1-onto-> A -> `' F Fn A )
8 fndifnfp 
 |-  ( `' F Fn A -> dom ( `' F \ _I ) = { x e. A | ( `' F ` x ) =/= x } )
9 6 7 8 3syl 
 |-  ( F : A -1-1-onto-> A -> dom ( `' F \ _I ) = { x e. A | ( `' F ` x ) =/= x } )
10 f1ofn 
 |-  ( F : A -1-1-onto-> A -> F Fn A )
11 fndifnfp 
 |-  ( F Fn A -> dom ( F \ _I ) = { x e. A | ( F ` x ) =/= x } )
12 10 11 syl 
 |-  ( F : A -1-1-onto-> A -> dom ( F \ _I ) = { x e. A | ( F ` x ) =/= x } )
13 5 9 12 3eqtr4d 
 |-  ( F : A -1-1-onto-> A -> dom ( `' F \ _I ) = dom ( F \ _I ) )