Metamath Proof Explorer


Definition df-evpm

Description: Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018)

Ref Expression
Assertion df-evpm
|- pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cevpm
 |-  pmEven
1 vd
 |-  d
2 cvv
 |-  _V
3 cpsgn
 |-  pmSgn
4 1 cv
 |-  d
5 4 3 cfv
 |-  ( pmSgn ` d )
6 5 ccnv
 |-  `' ( pmSgn ` d )
7 c1
 |-  1
8 7 csn
 |-  { 1 }
9 6 8 cima
 |-  ( `' ( pmSgn ` d ) " { 1 } )
10 1 2 9 cmpt
 |-  ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) )
11 0 10 wceq
 |-  pmEven = ( d e. _V |-> ( `' ( pmSgn ` d ) " { 1 } ) )