Metamath Proof Explorer

Theorem pmtrfinv

Description: A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015)

Ref Expression
Hypotheses pmtrrn.t 
|- T = ( pmTrsp ` D )
pmtrrn.r 
|- R = ran T
Assertion pmtrfinv 
|- ( F e. R -> ( F o. F ) = ( _I |` D ) )

Proof

Step Hyp Ref Expression
1 pmtrrn.t 
 |-  T = ( pmTrsp ` D )
2 pmtrrn.r 
 |-  R = ran T
3 eqid 
 |-  dom ( F \ _I ) = dom ( F \ _I )
4 1 2 3 pmtrfrn 
 |-  ( F e. R -> ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) /\ F = ( T ` dom ( F \ _I ) ) ) )
5 4 simpld 
 |-  ( F e. R -> ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) )
6 1 pmtrf 
 |-  ( ( D e. _V /\ dom ( F \ _I ) C_ D /\ dom ( F \ _I ) ~~ 2o ) -> ( T ` dom ( F \ _I ) ) : D --> D )
7 5 6 syl 
 |-  ( F e. R -> ( T ` dom ( F \ _I ) ) : D --> D )
8 4 simprd 
 |-  ( F e. R -> F = ( T ` dom ( F \ _I ) ) )
9 8 feq1d 
 |-  ( F e. R -> ( F : D --> D <-> ( T ` dom ( F \ _I ) ) : D --> D ) )
10 7 9 mpbird 
 |-  ( F e. R -> F : D --> D )
11 fco 
 |-  ( ( F : D --> D /\ F : D --> D ) -> ( F o. F ) : D --> D )
12 11 anidms 
 |-  ( F : D --> D -> ( F o. F ) : D --> D )
13 ffn 
 |-  ( ( F o. F ) : D --> D -> ( F o. F ) Fn D )
14 10 12 13 3syl 
 |-  ( F e. R -> ( F o. F ) Fn D )
15 fnresi 
 |-  ( _I |` D ) Fn D
16 15 a1i 
 |-  ( F e. R -> ( _I |` D ) Fn D )
17 1 2 3 pmtrffv 
 |-  ( ( F e. R /\ x e. D ) -> ( F ` x ) = if ( x e. dom ( F \ _I ) , U. ( dom ( F \ _I ) \ { x } ) , x ) )
18 iftrue 
 |-  ( x e. dom ( F \ _I ) -> if ( x e. dom ( F \ _I ) , U. ( dom ( F \ _I ) \ { x } ) , x ) = U. ( dom ( F \ _I ) \ { x } ) )
19 17 18 sylan9eq 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> ( F ` x ) = U. ( dom ( F \ _I ) \ { x } ) )
20 19 fveq2d 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> ( F ` ( F ` x ) ) = ( F ` U. ( dom ( F \ _I ) \ { x } ) ) )
21 simpll 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> F e. R )
22 5 simp2d 
 |-  ( F e. R -> dom ( F \ _I ) C_ D )
23 22 ad2antrr 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> dom ( F \ _I ) C_ D )
24 1onn 
 |-  1o e. _om
25 5 simp3d 
 |-  ( F e. R -> dom ( F \ _I ) ~~ 2o )
26 df-2o 
 |-  2o = suc 1o
27 25 26 breqtrdi 
 |-  ( F e. R -> dom ( F \ _I ) ~~ suc 1o )
28 27 ad2antrr 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> dom ( F \ _I ) ~~ suc 1o )
29 simpr 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> x e. dom ( F \ _I ) )
30 dif1en 
 |-  ( ( 1o e. _om /\ dom ( F \ _I ) ~~ suc 1o /\ x e. dom ( F \ _I ) ) -> ( dom ( F \ _I ) \ { x } ) ~~ 1o )
31 24 28 29 30 mp3an2i 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> ( dom ( F \ _I ) \ { x } ) ~~ 1o )
32 en1uniel 
 |-  ( ( dom ( F \ _I ) \ { x } ) ~~ 1o -> U. ( dom ( F \ _I ) \ { x } ) e. ( dom ( F \ _I ) \ { x } ) )
33 31 32 syl 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> U. ( dom ( F \ _I ) \ { x } ) e. ( dom ( F \ _I ) \ { x } ) )
34 33 eldifad 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> U. ( dom ( F \ _I ) \ { x } ) e. dom ( F \ _I ) )
35 23 34 sseldd 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> U. ( dom ( F \ _I ) \ { x } ) e. D )
36 1 2 3 pmtrffv 
 |-  ( ( F e. R /\ U. ( dom ( F \ _I ) \ { x } ) e. D ) -> ( F ` U. ( dom ( F \ _I ) \ { x } ) ) = if ( U. ( dom ( F \ _I ) \ { x } ) e. dom ( F \ _I ) , U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) , U. ( dom ( F \ _I ) \ { x } ) ) )
37 21 35 36 syl2anc 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> ( F ` U. ( dom ( F \ _I ) \ { x } ) ) = if ( U. ( dom ( F \ _I ) \ { x } ) e. dom ( F \ _I ) , U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) , U. ( dom ( F \ _I ) \ { x } ) ) )
38 iftrue 
 |-  ( U. ( dom ( F \ _I ) \ { x } ) e. dom ( F \ _I ) -> if ( U. ( dom ( F \ _I ) \ { x } ) e. dom ( F \ _I ) , U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) , U. ( dom ( F \ _I ) \ { x } ) ) = U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) )
39 34 38 syl 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> if ( U. ( dom ( F \ _I ) \ { x } ) e. dom ( F \ _I ) , U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) , U. ( dom ( F \ _I ) \ { x } ) ) = U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) )
40 25 adantr 
 |-  ( ( F e. R /\ x e. D ) -> dom ( F \ _I ) ~~ 2o )
41 en2other2 
 |-  ( ( x e. dom ( F \ _I ) /\ dom ( F \ _I ) ~~ 2o ) -> U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) = x )
42 41 ancoms 
 |-  ( ( dom ( F \ _I ) ~~ 2o /\ x e. dom ( F \ _I ) ) -> U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) = x )
43 40 42 sylan 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) = x )
44 39 43 eqtrd 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> if ( U. ( dom ( F \ _I ) \ { x } ) e. dom ( F \ _I ) , U. ( dom ( F \ _I ) \ { U. ( dom ( F \ _I ) \ { x } ) } ) , U. ( dom ( F \ _I ) \ { x } ) ) = x )
45 37 44 eqtrd 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> ( F ` U. ( dom ( F \ _I ) \ { x } ) ) = x )
46 20 45 eqtrd 
 |-  ( ( ( F e. R /\ x e. D ) /\ x e. dom ( F \ _I ) ) -> ( F ` ( F ` x ) ) = x )
47 10 ffnd 
 |-  ( F e. R -> F Fn D )
48 fnelnfp 
 |-  ( ( F Fn D /\ x e. D ) -> ( x e. dom ( F \ _I ) <-> ( F ` x ) =/= x ) )
49 47 48 sylan 
 |-  ( ( F e. R /\ x e. D ) -> ( x e. dom ( F \ _I ) <-> ( F ` x ) =/= x ) )
50 49 necon2bbid 
 |-  ( ( F e. R /\ x e. D ) -> ( ( F ` x ) = x <-> -. x e. dom ( F \ _I ) ) )
51 50 biimpar 
 |-  ( ( ( F e. R /\ x e. D ) /\ -. x e. dom ( F \ _I ) ) -> ( F ` x ) = x )
52 fveq2 
 |-  ( ( F ` x ) = x -> ( F ` ( F ` x ) ) = ( F ` x ) )
53 id 
 |-  ( ( F ` x ) = x -> ( F ` x ) = x )
54 52 53 eqtrd 
 |-  ( ( F ` x ) = x -> ( F ` ( F ` x ) ) = x )
55 51 54 syl 
 |-  ( ( ( F e. R /\ x e. D ) /\ -. x e. dom ( F \ _I ) ) -> ( F ` ( F ` x ) ) = x )
56 46 55 pm2.61dan 
 |-  ( ( F e. R /\ x e. D ) -> ( F ` ( F ` x ) ) = x )
57 fvco2 
 |-  ( ( F Fn D /\ x e. D ) -> ( ( F o. F ) ` x ) = ( F ` ( F ` x ) ) )
58 47 57 sylan 
 |-  ( ( F e. R /\ x e. D ) -> ( ( F o. F ) ` x ) = ( F ` ( F ` x ) ) )
59 fvresi 
 |-  ( x e. D -> ( ( _I |` D ) ` x ) = x )
60 59 adantl 
 |-  ( ( F e. R /\ x e. D ) -> ( ( _I |` D ) ` x ) = x )
61 56 58 60 3eqtr4d 
 |-  ( ( F e. R /\ x e. D ) -> ( ( F o. F ) ` x ) = ( ( _I |` D ) ` x ) )
62 14 16 61 eqfnfvd 
 |-  ( F e. R -> ( F o. F ) = ( _I |` D ) )