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 = ( 𝑑 ∈ 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 } ) )