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 = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cevpm	⊢ pmEven
1		vd	⊢ 𝑑
2		cvv	⊢ V
3		cpsgn	⊢ pmSgn
4	1	cv	⊢ 𝑑
5	4 3	cfv	⊢ ( pmSgn ‘ 𝑑 )
6	5	ccnv	⊢ ◡ ( pmSgn ‘ 𝑑 )
7		c1	⊢ 1
8	7	csn	⊢ { 1 }
9	6 8	cima	⊢ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } )
10	1 2 9	cmpt	⊢ ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) )
11	0 10	wceq	⊢ pmEven = ( 𝑑 ∈ V ↦ ( ◡ ( pmSgn ‘ 𝑑 ) “ { 1 } ) )