Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pmtrfconj Structured version   Visualization version   Unicode version

Theorem pmtrfconj 17100
 Description: Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.)
Hypotheses
Ref Expression
pmtrrn.t pmTrsp
pmtrrn.r
Assertion
Ref Expression
pmtrfconj

Proof of Theorem pmtrfconj
StepHypRef Expression
1 pmtrrn.t . . . . 5 pmTrsp
2 pmtrrn.r . . . . 5
31, 2pmtrfb 17099 . . . 4
43simp1bi 1022 . . 3
6 simpr 463 . . . 4
71, 2pmtrff1o 17097 . . . . 5
87adantr 467 . . . 4
9 f1oco 5834 . . . 4
106, 8, 9syl2anc 666 . . 3
11 f1ocnv 5824 . . . 4
13 f1oco 5834 . . 3
1410, 12, 13syl2anc 666 . 2
15 f1of 5812 . . . . . . 7
167, 15syl 17 . . . . . 6
1716adantr 467 . . . . 5
18 f1omvdconj 17080 . . . . 5
1917, 6, 18syl2anc 666 . . . 4
20 f1of1 5811 . . . . . 6
2120adantl 468 . . . . 5
22 difss 3559 . . . . . . . 8
23 dmss 5033 . . . . . . . 8
2422, 23ax-mp 5 . . . . . . 7
25 fdm 5731 . . . . . . 7
2624, 25syl5sseq 3479 . . . . . 6
2717, 26syl 17 . . . . 5
285, 27ssexd 4549 . . . . 5
29 f1imaeng 7626 . . . . 5
3021, 27, 28, 29syl3anc 1267 . . . 4
3119, 30eqbrtrd 4422 . . 3
323simp3bi 1024 . . . 4