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 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 R D V dom F I D dom F I 2 𝑜 F = T dom F I
5 4 simpld F R D V dom F I D dom F I 2 𝑜
6 1 pmtrf D V dom F I D dom F I 2 𝑜 T dom F I : D D
7 5 6 syl F R T dom F I : D D
8 4 simprd F R F = T dom F I
9 8 feq1d F R F : D D T dom F I : D D
10 7 9 mpbird F R F : D D
11 1 2 pmtrfinv F R F F = I D
12 10 10 11 11 fcof1od F R F : D 1-1 onto D