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

Definition df-pmtr 27364
 Description: Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
Assertion
Ref Expression
df-pmtr pmTrsp
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-pmtr
StepHypRef Expression
1 cpmtr 27363 . 2 pmTrsp
2 vd . . 3
3 cvv 2958 . . 3
4 vp . . . 4
5 vy . . . . . . 7
65cv 1652 . . . . . 6
7 c2o 6720 . . . . . 6
8 cen 7108 . . . . . 6
96, 7, 8wbr 4214 . . . . 5
102cv 1652 . . . . . 6
1110cpw 3801 . . . . 5
129, 5, 11crab 2711 . . . 4
13 vz . . . . 5
1413, 4wel 1727 . . . . . 6
154cv 1652 . . . . . . . 8
1613cv 1652 . . . . . . . . 9
1716csn 3816 . . . . . . . 8
1815, 17cdif 3319 . . . . . . 7
1918cuni 4017 . . . . . 6
2014, 19, 16cif 3741 . . . . 5
2113, 10, 20cmpt 4268 . . . 4
224, 12, 21cmpt 4268 . . 3
232, 3, 22cmpt 4268 . 2
241, 23wceq 1653 1 pmTrsp
 Colors of variables: wff set class This definition is referenced by:  pmtrfval  27372
 Copyright terms: Public domain W3C validator