Metamath Proof Explorer

Theorem pmtrfcnv

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

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

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 1 2 pmtrfinv 
 |-  ( F e. R -> ( F o. F ) = ( _I |` D ) )
12 10 10 11 11 2fcoidinvd 
 |-  ( F e. R -> `' F = F )