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 } ) )