Metamath Proof Explorer


Theorem pmtrff1o

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

Ref Expression
Hypotheses pmtrrn.t
|- T = ( pmTrsp ` D )
pmtrrn.r
|- R = ran T
Assertion pmtrff1o
|- ( F e. R -> F : D -1-1-onto-> 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 1 2 pmtrfinv
 |-  ( F e. R -> ( F o. F ) = ( _I |` D ) )
12 10 10 11 11 fcof1od
 |-  ( F e. R -> F : D -1-1-onto-> D )