Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmtrfconj Structured version   Unicode version

Theorem pmtrfconj 27422
 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 27421 . . . 4
43simp1bi 973 . . 3
6 simpr 449 . . . 4
71, 2pmtrff1o 27419 . . . . 5
87adantr 453 . . . 4
9 f1oco 5727 . . . 4
106, 8, 9syl2anc 644 . . 3
11 f1ocnv 5716 . . . 4
13 f1oco 5727 . . 3
1410, 12, 13syl2anc 644 . 2
15 f1of 5703 . . . . . . 7
167, 15syl 16 . . . . . 6
1716adantr 453 . . . . 5
18 f1omvdconj 27404 . . . . 5
1917, 6, 18syl2anc 644 . . . 4
20 f1of1 5702 . . . . . 6
2120adantl 454 . . . . 5
22 difss 3460 . . . . . . . 8
23 dmss 5098 . . . . . . . 8
2422, 23ax-mp 5 . . . . . . 7
25 fdm 5624 . . . . . . 7
2624, 25syl5sseq 3382 . . . . . 6
2717, 26syl 16 . . . . 5
285, 27ssexd 4379 . . . . 5
29 f1imaeng 7196 . . . . 5
3021, 27, 28, 29syl3anc 1185 . . . 4
3119, 30eqbrtrd 4257 . . 3
323simp3bi 975 . . . 4